arXiv subjects

Shaowei Lin

Publications and source records attributed to Shaowei Lin.

At least 19 recordsLinked to original sources

arXiv2025

Action-Driven Processes for Continuous-Time Control

At the heart of reinforcement learning are actions -- decisions made in response to observations of the environment. Actions are equally fundamental in the modeling of stochastic processes, as they trigger discontinuous state transitions and enable the flow of information through large, complex systems. In this paper, we unify the perspectives of stochastic processes and reinforcement learning through action-driven processes, and illustrate their application to spiking neural networks. Leveraging ideas from control-as-inference, we show that minimizing the Kullback-Leibler divergence between a policy-driven true distribution and a reward-driven model distribution for a suitably defined action-driven process is equivalent to maximum entropy reinforcement learning.

stat.ML↗

arXiv2025

A benchmark for vericoding: formally verified program synthesis

We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark

cs.SE↗

arXiv2024

Loss-driven miniaturized bound state in continuum biosensing system

Optical metasurface has brought a revolution in label-free molecular sensing, attracting extensive attention. Currently, such sensing approaches are being designed to respond to peak wavelengths with a higher Q factor in the visible and near-infrared regions.Nevertheless, a higher Q factor that enhances light confinement will inevitably deteriorate the wavelength sensitivity and complicate the sensing system. We propose a Q-switched sensing mechanism, which enables the real part of the refractive index to effectively perturbate the damping loss of the oscillator, resulting in a boost of peak intensity.Consequently, a higher Q factor in Q-switched sensor can further enhance the peak sensitivity while remaining compatible with broadband light sources, simultaneously meeting the requirements of high performance and a compact system.This is achieved in a unique 3D bound-state-in-continuum (BIC) metasurface which can be mass-produced by wafer-scale aluminum-nanoimprinting technology and provides a peak intensity sensitivity up to 928 %/RIU.Therefore, a miniaturized BIC biosensing system is realized, with a limit of detection to 10E-5 refractive index units and 129 aM extracellular vesicles in clinical lung cancer diagnosis, both of which are magnitudes lower than those of current state-of-the-art biosensors. It further demonstrates significant potential for home cancer self-testing equipment for post-operative follow-up. This Q-switched sensing mechanism offers a new perspective for the commercialization of advanced and practical BIC optical biosensing systems in real-setting scenarios.

physics.optics↗

arXiv2021

A Blockchain-Based Approach for Collaborative Formalization of Mathematics and Programs

Formalization of mathematics is the process of digitizing mathematical knowledge, which allows for formal proof verification as well as efficient semantic searches. Given the large and ever-increasing gap between the set of formalized and unformalized mathematical knowledge, there is a clear need to encourage more computer scientists and mathematicians to solve and formalize mathematical problems together. With blockchain technology, we are able to decentralize this process, provide time-stamped verification of authorship and encourage collaboration through implementation of incentive mechanisms via smart contracts. Currently, the formalization of mathematics is done through the use of proof assistants, which can be used to verify programs and protocols as well. Furthermore, with the advancement in artificial intelligence (AI), particularly machine learning, we can apply automated AI reasoning tools in these proof assistants and (at least partially) automate the process of synthesizing proofs. In our paper, we demonstrate a blockchain-based system for collaborative formalization of mathematics and programs incorporating both human labour as well as automated AI tools. We explain how Token-Curated Registries (TCR) and smart contracts are used to ensure appropriate documents are recorded and encourage collaboration through implementation of incentive mechanisms respectively. Using an illustrative example, we show how formalized proofs of different sorting algorithms can be produced collaboratively in our proposed blockchain system.

cs.MA↗

arXiv2021

Word2rate: training and evaluating multiple word embeddings as statistical transitions

Using pretrained word embeddings has been shown to be a very effective way in improving the performance of natural language processing tasks. In fact almost any natural language tasks that can be thought of has been improved by these pretrained embeddings. These tasks range from sentiment analysis, translation, sequence prediction amongst many others. One of the most successful word embeddings is the Word2vec CBOW model proposed by Mikolov trained by the negative sampling technique. Mai et al. modifies this objective to train CMOW embeddings that are sensitive to word order. We used a modified version of the negative sampling objective for our context words, modelling the context embeddings as a Taylor series of rate matrices. We show that different modes of the Taylor series produce different types of embeddings. We compare these embeddings to their similar counterparts like CBOW and CMOW and show that they achieve comparable performance. We also introduce a novel left-right context split objective that improves performance for tasks sensitive to word order. Our Word2rate model is grounded in a statistical foundation using rate matrices while being competitive in variety of language tasks.

cs.CL↗

arXiv2020

Dependently Typed Knowledge Graphs

Reasoning over knowledge graphs is traditionally built upon a hierarchy of languages in the Semantic Web Stack. Starting from the Resource Description Framework (RDF) for knowledge graphs, more advanced constructs have been introduced through various syntax extensions to add reasoning capabilities to knowledge graphs. In this paper, we show how standardized semantic web technologies (RDF and its query language SPARQL) can be reproduced in a unified manner with dependent type theory. In addition to providing the basic functionalities of knowledge graphs, dependent types add expressiveness in encoding both entities and queries, explainability in answers to queries through witnesses, and compositionality and automation in the construction of witnesses. Using the Coq proof assistant, we demonstrate how to build and query dependently typed knowledge graphs as a proof of concept for future works in this direction.

cs.FL↗

arXiv2019

Biologically Plausible Sequence Learning with Spiking Neural Networks

Motivated by the celebrated discrete-time model of nervous activity outlined by McCulloch and Pitts in 1943, we propose a novel continuous-time model, the McCulloch-Pitts network (MPN), for sequence learning in spiking neural networks. Our model has a local learning rule, such that the synaptic weight updates depend only on the information directly accessible by the synapse. By exploiting asymmetry in the connections between binary neurons, we show that MPN can be trained to robustly memorize multiple spatiotemporal patterns of binary vectors, generalizing the ability of the symmetric Hopfield network to memorize static spatial patterns. In addition, we demonstrate that the model can efficiently learn sequences of binary pictures as well as generative models for experimental neural spike-train data. Our learning rule is consistent with spike-timing-dependent plasticity (STDP), thus providing a theoretical ground for the systematic design of biologically inspired networks with large and robust long-range sequence storage capacity.

cond-mat.dis-nn↗

arXiv2017

Variational Probability Flow for Biologically Plausible Training of Deep Neural Networks

The quest for biologically plausible deep learning is driven, not just by the desire to explain experimentally-observed properties of biological neural networks, but also by the hope of discovering more efficient methods for training artificial networks. In this paper, we propose a new algorithm named Variational Probably Flow (VPF), an extension of minimum probability flow for training binary Deep Boltzmann Machines (DBMs). We show that weight updates in VPF are local, depending only on the states and firing rates of the adjacent neurons. Unlike contrastive divergence, there is no need for Gibbs confabulations; and unlike backpropagation, alternating feedforward and feedback phases are not required. Moreover, the learning algorithm is effective for training DBMs with intra-layer connections between the hidden nodes. Experiments with MNIST and Fashion MNIST demonstrate that VPF learns reasonable features quickly, reconstructs corrupted images more accurately, and generates samples with a high estimated log-likelihood. Lastly, we note that, interestingly, if an asymmetric version of VPF exists, the weight updates directly explain experimental results in Spike-Timing-Dependent Plasticity (STDP).

cs.LG↗

arXiv2016

Fast Adaptation of Activity Sensing Policies in Mobile Devices

With the proliferation of sensors, such as accelerometers, in mobile devices, activity and motion tracking has become a viable technology to understand and create an engaging user experience. This paper proposes a fast adaptation and learning scheme of activity tracking policies when user statistics are unknown a priori, varying with time, and inconsistent for different users. In our stochastic optimization, user activities are required to be synchronized with a backend under a cellular data limit to avoid overcharges from cellular operators. The mobile device is charged intermittently using wireless or wired charging for receiving the required energy for transmission and sensing operations. Firstly, we propose an activity tracking policy by formulating a stochastic optimization as a constrained Markov decision process (CMDP). Secondly, we prove that the optimal policy of the CMDP has a threshold structure using a Lagrangian relaxation approach and the submodularity concept. We accordingly present a fast Q-learning algorithm by considering the policy structure to improve the convergence speed over that of conventional Q-learning. Finally, simulation examples are presented to support the theoretical findings of this paper.

cs.HC↗

arXiv2016

Rate-distortion Balanced Data Compression for Wireless Sensor Networks

This paper presents a data compression algorithm with error bound guarantee for wireless sensor networks (WSNs) using compressing neural networks. The proposed algorithm minimizes data congestion and reduces energy consumption by exploring spatio-temporal correlations among data samples. The adaptive rate-distortion feature balances the compressed data size (data rate) with the required error bound guarantee (distortion level). This compression relieves the strain on energy and bandwidth resources while collecting WSN data within tolerable error margins, thereby increasing the scale of WSNs. The algorithm is evaluated using real-world datasets and compared with conventional methods for temporal and spatial data compression. The experimental validation reveals that the proposed algorithm outperforms several existing WSN data compression methods in terms of compression efficiency and signal reconstruction. Moreover, an energy analysis shows that compressing the data can reduce the energy expenditure, and hence expand the service lifespan by several folds.

cs.NI↗

arXiv2016

Mobile Big Data Analytics Using Deep Learning and Apache Spark

The proliferation of mobile devices, such as smartphones and Internet of Things (IoT) gadgets, results in the recent mobile big data (MBD) era. Collecting MBD is unprofitable unless suitable analytics and learning methods are utilized for extracting meaningful information and hidden patterns from data. This article presents an overview and brief tutorial of deep learning in MBD analytics and discusses a scalable learning framework over Apache Spark. Specifically, a distributed deep learning is executed as an iterative MapReduce computing on many Spark workers. Each Spark worker learns a partial deep model on a partition of the overall MBD, and a master deep model is then built by averaging the parameters of all partial models. This Spark-based framework speeds up the learning of deep models consisting of many hidden layers and millions of parameters. We use a context-aware activity recognition application with a real-world dataset containing millions of samples to validate our framework and assess its speedup effectiveness.

cs.DC↗

arXiv2015

Deep Activity Recognition Models with Triaxial Accelerometers

Despite the widespread installation of accelerometers in almost all mobile phones and wearable devices, activity recognition using accelerometers is still immature due to the poor recognition accuracy of existing recognition methods and the scarcity of labeled training data. We consider the problem of human activity recognition using triaxial accelerometers and deep learning paradigms. This paper shows that deep activity recognition models (a) provide better recognition accuracy of human activities, (b) avoid the expensive design of handcrafted features in existing systems, and (c) utilize the massive unlabeled acceleration samples for unsupervised feature extraction. Moreover, a hybrid approach of deep learning and hidden Markov models (DL-HMM) is presented for sequential activity recognition. This hybrid approach integrates the hierarchical representations of deep activity recognition models with the stochastic modeling of temporal sequences in the hidden Markov models. We show substantial recognition improvement on real world datasets over state-of-the-art methods of human activity recognition using triaxial accelerometers.

cs.LG↗

arXiv2015

Toward a Robust Sparse Data Representation for Wireless Sensor Networks

Compressive sensing has been successfully used for optimized operations in wireless sensor networks. However, raw data collected by sensors may be neither originally sparse nor easily transformed into a sparse data representation. This paper addresses the problem of transforming source data collected by sensor nodes into a sparse representation with a few nonzero elements. Our contributions that address three major issues include: 1) an effective method that extracts population sparsity of the data, 2) a sparsity ratio guarantee scheme, and 3) a customized learning algorithm of the sparsifying dictionary. We introduce an unsupervised neural network to extract an intrinsic sparse coding of the data. The sparse codes are generated at the activation of the hidden layer using a sparsity nomination constraint and a shrinking mechanism. Our analysis using real data samples shows that the proposed method outperforms conventional sparsity-inducing methods.

cs.NI↗

arXiv2015

Markov Decision Processes with Applications in Wireless Sensor Networks: A Survey

Wireless sensor networks (WSNs) consist of autonomous and resource-limited devices. The devices cooperate to monitor one or more physical phenomena within an area of interest. WSNs operate as stochastic systems because of randomness in the monitored environments. For long service time and low maintenance cost, WSNs require adaptive and robust methods to address data exchange, topology formulation, resource and power optimization, sensing coverage and object detection, and security challenges. In these problems, sensor nodes are to make optimized decisions from a set of accessible strategies to achieve design goals. This survey reviews numerous applications of the Markov decision process (MDP) framework, a powerful decision-making tool to develop adaptive algorithms and protocols for WSNs. Furthermore, various solution methods are discussed and compared to serve as a guide for using MDPs in WSNs.

cs.NI↗

arXiv2014

Marginal likelihood and model selection for Gaussian latent tree and forest models

Gaussian latent tree models, or more generally, Gaussian latent forest models have Fisher-information matrices that become singular along interesting submodels, namely, models that correspond to subforests. For these singularities, we compute the real log-canonical thresholds (also known as stochastic complexities or learning coefficients) that quantify the large-sample behavior of the marginal likelihood in Bayesian inference. This provides the information needed for a recently introduced generalization of the Bayesian information criterion. Our mathematical developments treat the general setting of Laplace integrals whose phase functions are sums of squared differences between monomials and constants. We clarify how in this case real log-canonical thresholds can be computed using polyhedral geometry, and we show how to apply the general theory to the Laplace integrals associated with Gaussian latent tree and forest models. In simulations and a data example, we demonstrate how the mathematical knowledge can be applied in model selection.

stat.ME↗

arXiv2014

Efficient Data Compression with Error Bound Guarantee in Wireless Sensor Networks

We present a data compression and dimensionality reduction scheme for data fusion and aggregation applications to prevent data congestion and reduce energy consumption at network connecting points such as cluster heads and gateways. Our in-network approach can be easily tuned to analyze the data temporal or spatial correlation using an unsupervised neural network scheme, namely the autoencoders. In particular, our algorithm extracts intrinsic data features from previously collected historical samples to transform the raw data into a low dimensional representation. Moreover, the proposed framework provides an error bound guarantee mechanism. We evaluate the proposed solution using real-world data sets and compare it with traditional methods for temporal and spatial data compression. The experimental validation reveals that our approach outperforms several existing wireless sensor network's data compression methods in terms of compression efficiency and signal reconstruction.

cs.NI↗

arXiv2014

Machine Learning in Wireless Sensor Networks: Algorithms, Strategies, and Applications

Wireless sensor networks monitor dynamic environments that change rapidly over time. This dynamic behavior is either caused by external factors or initiated by the system designers themselves. To adapt to such conditions, sensor networks often adopt machine learning techniques to eliminate the need for unnecessary redesign. Machine learning also inspires many practical solutions that maximize resource utilization and prolong the lifespan of the network. In this paper, we present an extensive literature review over the period 2002-2013 of machine learning methods that were used to address common issues in wireless sensor networks (WSNs). The advantages and disadvantages of each proposed algorithm are evaluated against the corresponding problem. We also provide a comparative guide to aid WSN designers in developing suitable machine learning solutions for their specific application challenges.

cs.NI↗

arXiv2014

Area Coverage Under Low Sensor Density

This paper presents a solution to the problem of monitoring a region of interest (RoI) using a set of nodes that is not sufficient to achieve the required degree of monitoring coverage. In particular, sensing coverage of wireless sensor networks (WSNs) is a crucial issue in projects due to failure of sensors. The lack of sensor equipment resources hinders the traditional method of using mobile robots to move around the RoI to collect readings. Instead, our solution employs supervised neural networks to produce the values of the uncovered locations by extracting the non-linear relation among randomly deployed sensor nodes throughout the area. Moreover, we apply a hybrid backpropagation method to accelerate the learning convergence speed to a local minimum solution. We use a real-world data set from meteorological deployment for experimental validation and analysis.

cs.NI↗