arXiv subjects

Mengyu Zhao

Publications and source records attributed to Mengyu Zhao.

10 recordsLinked to original sources

arXiv2026

Snapshot Compressive Imaging under Saturation: Theory, Mask Design, and Reconstruction

Snapshot compressive imaging (SCI) acquires high-dimensional data cubes, such as videos and hyperspectral images, by optically multiplexing multiple coded frames into a single two-dimensional measurement. While this multiplexing enables high acquisition efficiency, it also increases the risk of sensor saturation: the accumulated intensity may exceed the detector dynamic range, causing clipped measurements that violate the standard linear SCI model. This paper studies SCI reconstruction under such saturated measurements from both theoretical and algorithmic perspectives. We model saturation as an element-wise clipping nonlinearity and derive a finite-sample recovery bound for compression-based SCI. The bound explicitly relates the reconstruction error to the Bernoulli mask density, the compression rate of the signal class, measurement noise, and the expected fraction of saturated measurements. The analysis reveals a principled mask-design rule: under saturation, the optimal Bernoulli mask density remains below one-half and decreases as saturation becomes stronger. Motivated by this result, we optimize mask patterns for saturated acquisition and introduce a saturation-aware plug-and-play reconstruction framework, termed \emph{Saturation-Aware PnP Net} (SAPnet), which enforces consistency with both unsaturated and clipped measurements. Experiments on standard video SCI benchmarks validate the theoretical predictions and show that SAPnet substantially improves reconstruction quality over conventional PnP-based methods, especially in strongly saturated regimes.

eess.IV↗

arXiv2026

Analog photonic simulator for large-scale transport

Transport equations describe how physical quantities -- such as mass, energy, momentum, concentration, probability, or fields -- are carried, propagated, or redistributed through space and time, forming a foundational class of partial differential equations across science and engineering. However, high-dimensional partial differential equations are difficult to represent on digital grids because the number of degrees of freedom grows exponentially with dimension. Continuous-variable quantum photonics on the other hand can represent and evolve these large-scale fields without first discretizing space into a discrete grid. We demonstrate a large-scale analog photonic simulator for the constant-coefficient advection equation, a transport equation that is a fundamental benchmark for scientific computing. The solution of a $d$-variable advection equation is encoded into $d$ optical modes, so that the partial differential equation evolution maps directly to programmable phase-space displacements generated by optical quadrature momenta. Using a time-domain continuous-variable quantum photonic platform, we validate programmable control with $20,000$ single-mode squeezed states and $20,000$ two-mode squeezed states, and implement transport dynamics on a $20,000$-mode cluster-state resource. Homodyne measurements then verifies mode-resolved displacement control, which can provide first and second-order moment information of the solution to the advection equation, with final achievable relative error as low as $0.8\%$ and $0.92\%$ for first and second-order moment observables respectively. Our results establish continuous-variable photonics as a suitable programmable analog platform for large-scale advection equations.

quant-ph↗

arXiv2026

Shot-Aware Frame Sampling for Video Understanding

Video frame sampling is essential for efficient long-video understanding with Vision-Language Models (VLMs), since dense inputs are costly and often exceed context limits. Yet when only a small number of frames can be retained, existing samplers often fail to balance broad video coverage with brief but critical events, which can lead to unreliable downstream predictions. To address this issue, we present InfoShot, a task-agnostic, shot-aware frame sampler for long-video understanding. InfoShot first partitions a video into semantically consistent shots, and then selects two complementary keyframes from each shot: one to represent the main content and one to capture unusual within-shot changes. This design is guided by an information-theoretic objective that encourages the sampled set to retain high information about both shot structure and sparse within-shot deviations. In this way, it improves the chance of preserving both overall video context and short decision-critical moments without requiring any retraining. To better evaluate such short-lived events, we further introduce SynFlash, a synthetic benchmark with controllable sub-second anomaly patterns and frame-level ground truth, and we also evaluate InfoShot on existing anomaly datasets and general video understanding tasks. Experiments show that InfoShot improves anomaly hit rate and downstream Video-QA accuracy under frame number constraints, while matching or outperforming strong baselines on standard video understanding benchmarks.

cs.CV↗

arXiv2025

Efficient Formal Verification of Quantum Error Correcting Programs

Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.

cs.PL↗

arXiv2025

Theoretical Characterization of Effect of Masks in Snapshot Compressive Imaging

Snapshot compressive imaging (SCI) refers to the recovery of three-dimensional data cubes-such as videos or hyperspectral images-from their two-dimensional projections, which are generated by a special encoding of the data with a mask. SCI systems commonly use binary-valued masks that follow certain physical constraints. Optimizing these masks subject to these constraints is expected to improve system performance. However, prior theoretical work on SCI systems focuses solely on independently and identically distributed (i.i.d.) Gaussian masks, which do not permit such optimization. On the other hand, existing practical mask optimizations rely on computationally intensive joint optimizations that provide limited insight into the role of masks and are expected to be sub-optimal due to the non-convexity and complexity of the optimization. In this paper, we analytically characterize the performance of SCI systems employing binary masks and leverage our analysis to optimize hardware parameters. Our findings provide a comprehensive and fundamental understanding of the role of binary masks - with both independent and dependent elements - and their optimization. We also present simulation results that confirm our theoretical findings and further illuminate different aspects of mask design.

cs.IT↗

arXiv2024

One-Sided Device-Independent Random Number Generation Through Fiber Channels

Randomness is an essential resource and plays important roles in various applications ranging from cryptography to simulation of complex systems. Certified randomness from quantum process is ensured to have the element of privacy but usually relies on the device's behavior. To certify randomness without the characterization for device, it is crucial to realize the one-sided device-independent random number generation based on quantum steering, which guarantees security of randomness and relaxes the demands of one party's device. Here, we distribute quantum steering between two distant users through a 2 km fiber channel and generate quantum random numbers at the remote station with untrustworthy device. We certify the steering-based randomness by reconstructing covariance matrix of the Gaussian entangled state shared between distant parties. Then, the quantum random numbers with a generation rate of 7.06 Mbits/s are extracted from the measured amplitude quadrature fluctuation of the state owned by the remote party. Our results demonstrate the first realization of steering-based random numbers extraction in a practical fiber channel, which paves the way to the quantum random numbers generation in asymmetric networks.

quant-ph↗

arXiv2024

A Local Search Algorithm for MaxSMT(LIA)

MaxSAT modulo theories (MaxSMT) is an important generalization of Satisfiability modulo theories (SMT) with various applications. In this paper, we focus on MaxSMT with the background theory of Linear Integer Arithmetic, denoted as MaxSMT(LIA). We design the first local search algorithm for MaxSMT(LIA) called PairLS, based on the following novel ideas. A novel operator called pairwise operator is proposed for integer variables. It extends the original local search operator by simultaneously operating on two variables, enriching the search space. Moreover, a compensation-based picking heuristic is proposed to determine and distinguish the pairwise operations. Experiments are conducted to evaluate our algorithm on massive benchmarks. The results show that our solver is competitive with state-of-the-art MaxSMT solvers. Furthermore, we also apply the pairwise operation to enhance the local search algorithm of SMT, which shows its extensibility.

cs.SC↗

arXiv2024

Untrained Neural Nets for Snapshot Compressive Imaging: Theory and Algorithms

Snapshot compressive imaging (SCI) recovers high-dimensional (3D) data cubes from a single 2D measurement, enabling diverse applications like video and hyperspectral imaging to go beyond standard techniques in terms of acquisition speed and efficiency. In this paper, we focus on SCI recovery algorithms that employ untrained neural networks (UNNs), such as deep image prior (DIP), to model source structure. Such UNN-based methods are appealing as they have the potential of avoiding the computationally intensive retraining required for different source models and different measurement scenarios. We first develop a theoretical framework for characterizing the performance of such UNN-based methods. The theoretical framework, on the one hand, enables us to optimize the parameters of data-modulating masks, and on the other hand, provides a fundamental connection between the number of data frames that can be recovered from a single measurement to the parameters of the untrained NN. We also employ the recently proposed bagged-deep-image-prior (bagged-DIP) idea to develop SCI Bagged Deep Video Prior (SCI-BDVP) algorithms that address the common challenges faced by standard UNN solutions. Our experimental results show that in video SCI our proposed solution achieves state-of-the-art among UNN methods, and in the case of noisy measurements, it even outperforms supervised solutions.

cs.CV↗

arXiv2023

Theoretical Analysis of Binary Masks in Snapshot Compressive Imaging Systems

Snapshot compressive imaging (SCI) systems have gained significant attention in recent years. While previous theoretical studies have primarily focused on the performance analysis of Gaussian masks, practical SCI systems often employ binary-valued masks. Furthermore, recent research has demonstrated that optimized binary masks can significantly enhance system performance. In this paper, we present a comprehensive theoretical characterization of binary masks and their impact on SCI system performance. Initially, we investigate the scenario where the masks are binary and independently identically distributed (iid), revealing a noteworthy finding that aligns with prior numerical results. Specifically, we show that the optimal probability of non-zero elements in the masks is smaller than 0.5. This result provides valuable insights into the design and optimization of binary masks for SCI systems, facilitating further advancements in the field. Additionally, we extend our analysis to characterize the performance of SCI systems where the mask entries are not independent but are generated based on a stationary first-order Markov process. Overall, our theoretical framework offers a comprehensive understanding of the performance implications associated with binary masks in SCI systems.

cs.IT↗

arXiv2023

Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks

Constraint solving is an elementary way for verification of deep neural networks (DNN). In the domain of AI safety, a DNN might be modified in its structure and parameters for its repair or attack. For such situations, we propose the incremental DNN verification problem, which asks whether a safety property still holds after the DNN is modified. To solve the problem, we present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. We simulate the most important features of the configurations that infers the verification result of the searching branches in the old solving procedure (with respect to the original network), and heuristically check whether the proofs are still valid for the modified DNN. We implement our algorithm as an incremental solver called DeepInc, and exerimental results show that DeepInc is more efficient in most cases. For the cases that the property holds both before and after modification, the acceleration can be faster by several orders of magnitude, showing that DeepInc is outstanding in incrementally searching for counterexamples. Moreover, based on the framework, we propose the multi-objective DNN repair problem and give an algorithm based on our incremental SMT solving algorithm. Our repair method preserves more potential safety properties on the repaired DNNs compared with state-of-the-art.

cs.AI↗