arXiv subjects

Shangzhou Xia

Publications and source records attributed to Shangzhou Xia.

11 recordsLinked to original sources

arXiv2026

StabQ: Quantum Program Analysis via Weighted Stabilizer Representations

Quantum program analysis remains challenging due to the exponentially large state space of quantum programs and the difficulty of precisely characterizing their execution behavior. In particular, non-Clifford operations introduce additional complexity that limits the applicability of stabilizer-based techniques. Although stabilizer representations provide compact descriptions for Clifford circuits, their limited expressiveness prevents them from directly supporting general quantum program analysis. In this work, we propose StabQ, a symbolic execution framework for quantum program analysis based on stabilizer representations. StabQ extends stabilizer-based symbolic execution beyond Clifford-only programs by introducing a symbolic state representation that captures and propagates quantum state evolution while preserving execution semantics. Based on this representation, StabQ constructs a Tableau Chain that represents the evolution of intermediate symbolic states throughout program execution and enables reusable analysis of quantum program executions. Furthermore, StabQ incorporates tableau consolidation and global-phase recovery mechanisms to mitigate symbolic state growth during execution. Building upon the Tableau Chain, StabQ supports multiple quantum program analysis tasks, including quantum state reconstruction, entanglement analysis, and Clifford-property detection. We evaluate StabQ on three benchmark suites---Algorithms, MQT Bench, and QASMBench. The results demonstrate that StabQ constructs semantically consistent symbolic models, accurately preserves quantum state evolution, and effectively supports downstream analysis tasks across diverse quantum programs.

cs.SC↗

arXiv2026

QuanForge: A Mutation Testing Framework for Quantum Neural Networks

With the growing synergy between deep learning and quantum computing, Quantum Neural Networks (QNNs) have emerged as a promising paradigm by leveraging quantum parallelism and entanglement. However, testing QNNs remains underexplored due to their complex quantum dynamics and limited interpretability. Developing a mutation testing technique for QNNs is promising while requires addressing stochastic factors, including the inherent randomness of mutation operators and quantum measurements. To tackle these challenges, we propose QuanForge, a mutation testing framework specifically designed for QNNs. We first introduce statistical mutation killing to provide a more reliable criterion. QuanForge incorporates nine post-training mutation operators at both gate and parameter levels, capable of simulating various potential errors in quantum circuits. Finally, a mutant generation algorithm is formalized that systematically produces effective mutants, thereby enabling a robust and reliable mutation analysis. Through extensive experiments on benchmark datasets and QNN architectures, we show that QuanForge can effectively distinguish different test suites and localize vulnerable circuit regions, providing insights for data enhancement and structural assessment of QNNs. We also analyze the generation capabilities of different operators and evaluate performance under simulated noisy conditions to assess the practical feasibility of QuanForge for future quantum devices.

cs.SE↗

arXiv2026

QEMI: A Quantum Software Stacks Testing Framework via Equivalence Modulo Inputs

As quantum algorithms and hardware continue to evolve, ensuring the correctness of the quantum software stack (QSS) has become increasingly important. However, testing QSSes remains challenging due to the oracle problem, i.e., the lack of a reliable ground truth for expected program behavior. Existing metamorphic testing approaches often rely on equivalent circuit transformations, backend modifications, or parameter tuning to address this issue. In this work, inspired by Equivalence Modulo Inputs (EMI), we propose Quantum EMI (QEMI), a new testing approach for QSSes. Our key contributions include: (1) a random quantum program generator that produces code with dead code based on quantum control-flow structures, and (2) an adaptation of the EMI technique from classical compiler testing to generate variants by removing dead code. By comparing the behavior of these variants, we can detect potential bugs in QSS implementations. We applied QEMI to Qiskit, Q#, and Cirq, and successfully identified 11 crash bugs and 1 behavioral inconsistency. QEMI expands the limited set of testing techniques available for quantum software stacks by going beyond structural transformations and incorporating semantics-preserving ones into quantum program analysis.

cs.SE↗

arXiv2026

QSolver: A Quantum Constraint Solver

With the growing interest in quantum programs, ensuring their correctness is a fundamental challenge. Although constraint-solving techniques can overcome some limitations of traditional testing and verification, they have not yet been sufficiently explored in the context of quantum programs. To address this gap, we present QSolver, the first quantum constraint solver. QSolver provides a structured framework for handling five types of quantum constraints and incorporates an automated assertion generation module to verify quantum states. QSolver transforms quantum programs and multi-moment constraints into symbolic representations, and utilizes an SMT solver to obtain quantum states that satisfy these constraints. To validate the correctness of the generated input states, QSolver automatically generates assertion programs corresponding to each constraint. Experimental results show that QSolver efficiently processes commonly used quantum gates and demonstrates good scalability across quantum programs of different sizes.

quant-ph↗

arXiv2026

QSPE: Enumerating Skeletal Quantum Programs for Quantum Library Testing

The rapid advancement of quantum computing has led to the development of various quantum libraries, empowering compilation, simulation, and hardware backend interfaces. However, ensuring the correctness of these libraries remains a fundamental challenge due to the lack of mature testing methodologies. The state-of-the-art tools often rely on domain-specific configurations and expert knowledge, which limits their accessibility and scalability in practice. Furthermore, although these tools demonstrate strong performance, they adopt measurement-based for output validation in testing, which makes them produce false positive reports. To alleviate these limitations, we propose QSPE, a practical approach that follows the differential testing principle and extends the existing approach, SPE, for quantum libraries. QSPE is fully automated, requiring no pre-set configurations or domain expertise, and can effectively generate a large set of diverse program variants that comprehensively explore the quantum compilation space. To mitigate the possible false positive reports, we propose statevector-based validation as an alternative to measurement-based validation. In our experiments, the QSPE approach demonstrates remarkable effectiveness in generating 22,770 program variants across multiple quantum computing platforms. By avoiding $α$-equivalence at the quantum and classical program wise, QSPE can reduce redundant generation and save more than 90\% of execution cost. Finally, the statevector-based validation method assists QSPE to reduce false alarms and effectively detects 708 miscompilations across multiple quantum libraries. Notably, 81 of the discovered bugs have been officially approved and acknowledged by the Qiskit development team, demonstrating the practical impact of our approach.

quant-ph↗

arXiv2025

Evaluating Model Performance Under Worst-case Subpopulations

The performance of ML models degrades when the training population is different from that seen under operation. Towards assessing distributional robustness, we study the worst-case performance of a model over all subpopulations of a given size, defined with respect to core attributes Z. This notion of robustness can consider arbitrary (continuous) attributes Z, and automatically accounts for complex intersectionality in disadvantaged groups. We develop a scalable yet principled two-stage estimation procedure that can evaluate the robustness of state-of-the-art models. We prove that our procedure enjoys several finite-sample convergence guarantees, including dimension-free convergence. Instead of overly conservative notions based on Rademacher complexities, our evaluation error depends on the dimension of Z only through the out-of-sample error in estimating the performance conditional on Z. On real datasets, we demonstrate that our method certifies the robustness of a model and prevents deployment of unreliable models.

cs.LG↗

arXiv2025

Is Measurement Enough? Rethinking Output Validation in Quantum Program Testing

As quantum computing continues to emerge, ensuring the quality of quantum programs has become increasingly critical. Quantum program testing has emerged as a prominent research area within the scope of quantum software engineering. While numerous approaches have been proposed to address quantum program quality assurance, our analysis reveals that most existing methods rely on measurement-based validation in practice. However, due to the inherently probabilistic nature of quantum programs, measurement-based validation methods face significant limitations. To investigate these limitations, we conducted an empirical study of recent research on quantum program testing, analyzing measurement-based validation methods in the literature. Our analysis categorizes existing measurement-based validation methods into two groups: distribution-level validation and output-value-level validation. We then compare measurement-based validation with statevector-based validation methods to evaluate their pros and cons. Our findings demonstrate that measurement-based validation is suitable for straightforward assessments, such as verifying the existence of specific output values, while statevector-based validation proves more effective for complicated tasks such as assessing the program behaviors.

cs.SE↗

arXiv2025

NovaQ: Improving Quantum Program Testing through Diversity-Guided Test Case Generation

Quantum programs are designed to run on quantum computers, leveraging quantum circuits to solve problems that are intractable for classical machines. As quantum computing advances, ensuring the reliability of quantum programs has become increasingly important. This paper introduces NovaQ, a diversity-guided testing framework for quantum programs. NovaQ combines a distribution-based test case generator with a novelty-driven evaluation module. The generator produces diverse quantum state inputs by mutating circuit parameters, while the evaluator quantifies behavioral novelty based on internal circuit state metrics, including magnitude, phase, and entanglement. By selecting inputs that map to infrequently covered regions in the metric space, NovaQ effectively explores under-tested program behaviors. We evaluate NovaQ on quantum programs of varying sizes and complexities. Experimental results show that NovaQ consistently achieves higher test input diversity and detects more bugs than existing baseline approaches.

cs.SE↗

arXiv2025

Quantum Concolic Testing

This paper presents the first concolic testing framework explicitly designed for quantum programs. The framework introduces quantum constraint generation methods for quantum control statements that quantify quantum states and offers a symbolization method for quantum variables. Based on this framework, we generate path constraints for each concrete execution path of a quantum program. These constraints guide the exploration of new paths, with a quantum constraint solver determining outcomes to create novel input samples, thereby enhancing branch coverage. Our framework has been implemented in Python and integrated with Qiskit for practical evaluation. Experimental results show that our concolic testing framework improves branch coverage, generates high-quality quantum input samples, and detects bugs, demonstrating its effectiveness and efficiency in quantum programming and bug detection. Regarding branch coverage, our framework achieves more than 74.27% on quantum programs with under 5 qubits.

cs.SE↗

arXiv2023

Uniformly Bounded Regret in Dynamic Fair Allocation

We study a dynamic allocation problem in which $T$ sequentially arriving divisible resources are to be allocated to a number of agents with linear utilities. The marginal utilities of each resource to the agents are drawn stochastically from a known joint distribution, independently and identically across time, and the central planner makes immediate and irrevocable allocation decisions. Most works on dynamic resource allocation aim to maximize the utilitarian welfare, i.e., the efficiency of the allocation, which may result in unfair concentration of resources on certain high-utility agents while leaving others' demands under-fulfilled. In this paper, aiming at balancing efficiency and fairness, we instead consider a broad collection of welfare metrics, the Hölder means, which includes the Nash social welfare and the egalitarian welfare. To this end, we first study a fluid-based policy derived from a deterministic surrogate to the underlying problem and show that for all smooth Hölder mean welfare metrics it attains an $O(1)$ regret over the time horizon length $T$ against the hindsight optimum, i.e., the optimal welfare if all utilities were known in advance of deciding on allocations. However, when evaluated under the non-smooth egalitarian welfare, the fluid-based policy attains a regret of order $Θ(\sqrt{T})$. We then propose a new policy built thereupon, called Backward Infrequent Re-solving with Thresholding ($\mathsf{BIRT}$), which consists of re-solving the deterministic surrogate problem at most $O(\log\log T)$ times. We prove the $\mathsf{BIRT}$ policy attains an $O(1)$ regret against the hindsight optimal egalitarian welfare, independently of the time horizon length $T$. We conclude by presenting numerical experiments to corroborate our theoretical claims and to illustrate the significant performance improvement against several benchmark policies.

math.OC↗

arXiv2023

Static Entanglement Analysis of Quantum Programs

Quantum entanglement plays a crucial role in quantum computing. Entangling information has important implications for understanding the behavior of quantum programs and avoiding entanglement-induced errors. Entanglement analysis is a static code analysis technique that determines which qubit may entangle with another qubit and establishes an entanglement graph to represent the whole picture of interactions between entangled qubits. This paper presents the first static entanglement analysis method for quantum programs developed in the practical quantum programming language Q\#. Our method first constructs an interprocedural control flow graph (ICFG) for a Q\# program and then calculates the entanglement information not only within each module but also between modules of the program. The analysis results can help improve the reliability and security of quantum programs.

cs.SE↗