arXiv subjects

Jianjun Zhao

Publications and source records attributed to Jianjun Zhao.

At least 19 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

Branch and Bound for Relational Verification of Neural Networks

Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.

cs.LG↗

arXiv2026

NARU: A Benchmark for NARrative Evolution and Cultural Nuance Understanding in Japanese Extreme Long Video

Long-form video understanding encompasses tasks that go beyond retrieving isolated events, including tracking an evolving narrative and interpreting social meaning that may remain implicit. However, existing benchmarks rarely evaluate these capabilities jointly, particularly in high-context, non-English media. To address this gap, we introduce NARU, a benchmark designed to evaluate Narrative evolution and Reasoning on cultural Understanding in Japanese long-form video. NARU consists of 1,481 questions grounded in 155 videos totaling 146.8 hours, spanning four narrative and five cultural dimensions. To construct the benchmark at this scale, we propose a hierarchical memory-based annotation pipeline that transforms raw video into structured event, narrative, and cultural annotations, then generates questions via task-oriented synthesis and iterative shortcut removal. The construction process includes two native-speaker verification stages involving 68 annotators. Evaluations across eight model configurations reveal substantial limitations in both long-range narrative integration and culturally grounded reasoning. By exposing these persistent gaps, NARU offers a systematic testing ground for developing MLLMs capable of reliably interpreting long-form, high-context video.

cs.CV↗

arXiv2026

Benchmarking Quantum Software Testing with Scalable Quantum Programs

Quantum software testing (QST) checks whether quantum programs behave according to their intended specifications. A key requirement for QST research is a benchmark that supports rigorous empirical evaluation on programs that are testable and better reflect current software development practices. However, existing studies heavily rely on small hard-coded or circuit-level benchmarks, while available quantum programs are scattered across repositories without clear selection criteria, which limits fair comparison and systematic reproducibility. To this end, we present Qolumbina, a benchmark infrastructure for controlled QST experiments on scalable quantum programs. Qolumbina curates 40 programs from open-source repositories, turns them into test-ready subjects through systematic selection, refactoring, specifications, test case examples, unit tests, and standardized interfaces. We also propose QST-oriented criteria to characterize quantum programs along functionality, output behavior, development complexity, and quantum-specific execution complexity. Using these criteria, our empirical study shows that Qolumbina covers diverse testing-relevant properties and supports scalability analysis beyond fixed-size circuit benchmarks. Through controlled experiments with two recent QST approaches, we demonstrate the feasibility of using Qolumbina for execution-cost and fault-detection studies, and highlight backend-dependent effects that can influence QST result interpretation.

cs.SE↗

arXiv2026

Quantum vs. Classical Machine Learning: A Unified Empirical Comparison

Quantum computing has emerged as a promising computational paradigm for machine learning (ML), with the potential to offer computational advantages over classical approaches. At this stage, the evidence supporting the performance and advantages of quantum machine learning (QML) models relative to classical models is insufficient. To address this gap, this paper presents an empirical study on the performance of QML models and their classical counterparts. We compare seven model pairs spanning supervised learning and reinforcement learning. Our results indicate that the evaluated quantum machine learning models do not yet surpass the classical baselines in overall prediction performance, policy stability, or training time. Nevertheless, QML remains a promising approach for filtering noise and controlling false positives. Our research findings summarize the challenges facing quantum machine learning across hardware environments, training efficiency, and convergence stability, providing a foundation for research into the robustness and parameter optimization of QML. This work is publicly available at https://github.com/Z-537-437/QML.

cs.LG↗

arXiv2026

From Flat Language Labels to Typological Priors: Structured Language Conditioning for Multilingual Speech-to-Speech Translation

Compositional speech-to-speech translation (S2ST) systems built upon speech large language models (SpeechLLMs) have recently shown promising performance. However, existing S2ST systems often either neglect source-language information or encode it through a language-as-label paradigm, representing each source language as an independent flat embedding. Such a design overlooks systematic linguistic structure shared across languages, which may limit data-efficient multilingual adaptation when supervised S2ST data are scarce. To address this issue, we propose S2ST-Omni 2, a many-to-one compositional S2ST framework that systematically reformulates multilingual language conditioning from flat language labels to structured typological priors. Specifically, S2ST-Omni 2 revisits language conditioning at three levels: typology-informed hierarchical language encoding for structured source-language representation, dynamically-gated language-aware Dual-CTC for content-adaptive acoustic modulation, and typology-aware LLM prompting for decoder-side linguistic guidance. Experiments on CVSS-C show that S2ST-Omni 2 achieves superior average performance among representative S2ST approaches across BLEU, COMET, ASR-BLEU, and BLASER 2.0 under the adopted evaluation protocol. Ablation studies indicate that the proposed representation-level, acoustic-level, and decoding-level strategies provide complementary benefits. Moreover, controlled data-budget analyses and a Japanese-to-English evaluation using only approximately 3 hours of supervised training data suggest that explicit typological priors provide useful inductive biases for data-efficient multilingual S2ST.

cs.CL↗

arXiv2026

Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.

cs.AI↗

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

Software Testing in the Quantum World

Quantum computing offers significant speedups for simulating physical, chemical, and biological systems, and for optimization and machine learning. As quantum software grows in complexity, the classical simulation of quantum computers, which has long been essential for quality assurance, becomes infeasible. This shift requires new quality-assurance methods that operate directly on real quantum computers. This paper presents the key challenges in testing large-scale quantum software and offers software engineering perspectives for addressing them.

cs.SE↗

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 $\alpha$-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↗

arXiv2026

A Methodological Analysis of Empirical Studies in Quantum Software Testing

In quantum software engineering (QSE), quantum software testing (QST) has attracted increasing attention as quantum software systems grow in scale and complexity. Since QST evaluates quantum programs through execution under designed test inputs, empirical studies are widely used to assess the effectiveness of testing approaches. However, the design and reporting of empirical studies in QST remain highly diverse, and a shared methodological understanding has yet to emerge, making it difficult to interpret results and compare findings across studies. This paper presents a methodological analysis of empirical studies in QST through a systematic examination of 59 primary studies identified from a literature pool of size 384. We organize our analysis around ten research questions that cover key methodological dimensions of QST empirical studies, including objects under test, baseline comparison, testing setup, experimental configuration, and tool and artifact support. Through cross-study analysis along these dimensions, we characterize current empirical practices in QST, identify recurring limitations and inconsistencies, and highlight open methodological challenges. Based on our findings, we derive insights and recommendations to inform the design, execution, and reporting of future empirical studies in QST.

quant-ph↗

arXiv2025

A Comprehensive Study of Deep Learning Model Fixing Approaches

Deep Learning (DL) has been widely adopted in diverse industrial domains, including autonomous driving, intelligent healthcare, and aided programming. Like traditional software, DL systems are also prone to faults, whose malfunctioning may expose users to significant risks. Consequently, numerous approaches have been proposed to address these issues. In this paper, we conduct a large-scale empirical study on 16 state-of-the-art DL model fixing approaches, spanning model-level, layer-level, and neuron-level categories, to comprehensively evaluate their performance. We assess not only their fixing effectiveness (their primary purpose) but also their impact on other critical properties, such as robustness, fairness, and backward compatibility. To ensure comprehensive and fair evaluation, we employ a diverse set of datasets, model architectures, and application domains within a uniform experimental setup for experimentation. We summarize several key findings with implications for both industry and academia. For example, model-level approaches demonstrate superior fixing effectiveness compared to others. No single approach can achieve the best fixing performance while improving accuracy and maintaining all other properties. Thus, academia should prioritize research on mitigating these side effects. These insights highlight promising directions for future exploration in this field.

cs.LG↗

arXiv2025

QMon: Monitoring the Execution of Quantum Circuits with Mid-Circuit Measurement and Reset

Unlike classical software, where logging and runtime tracing can effectively reveal internal execution status, quantum circuits possess unique properties, such as the no-cloning theorem and measurement-induced collapse, that prevent direct observation or duplication of their states. These characteristics make it especially challenging to monitor the execution of quantum circuits, complicating essential tasks such as debugging and runtime monitoring. This paper presents QMON, a practical methodology that leverages mid-circuit measurements and reset operations to monitor the internal states of quantum circuits while preserving their original runtime behavior. QMON enables the instrumentation of monitoring operators at developer-specified locations within the circuit, allowing comparisons between expected and observed quantum-state probabilities at those locations. We evaluated QMON by analyzing its impact on circuit behavior, monitoring coverage, and effectiveness in bug localization. Experimental results involving 154 quantum circuits show that all circuits preserve their intended functionality after instrumentation and that QMON successfully detects and localizes various programming errors. Although monitoring coverage is limited by the need to preserve delicate quantum properties, such as entanglement, QMON effectively detects errors while introducing no or negligible disturbance to the original quantum states. QMON facilitates the development of more robust and reliable quantum software as the field continues to mature.

cs.SE↗

arXiv2025

When Abstraction Breaks Physics: Rethinking Modular Design in Quantum Software

Abstraction is a fundamental principle in classical software engineering, which enables modularity, reusability, and scalability. However, quantum programs adhere to fundamentally different semantics, such as unitarity, entanglement, the no-cloning theorem, and the destructive nature of measurement, which introduce challenges to the safe use of classical abstraction mechanisms. This paper identifies a fundamental conflict in quantum software engineering: abstraction practices that are syntactically valid may violate the physical constraints of quantum computation. We present three classes of failure cases where naive abstraction breaks quantum semantics and propose a set of design principles for physically sound abstraction mechanisms. We further propose research directions, including quantum-specific type systems, effect annotations, and contract-based module design. Our goal is to initiate a systematic rethinking of abstraction in quantum software engineering, based on quantum semantics and considering engineering scalability.

cs.SE↗

arXiv2025

M2QCode: A Model-Driven Framework for Generating Multi-Platform Quantum Programs

With the growing interest in quantum computing, the emergence of quantum supremacy has marked a pivotal milestone in the field. As a result, numerous quantum programming languages (QPLs) have been introduced to support the development of quantum algorithms. However, the application of Model-Driven Development (MDD) in quantum system engineering remains largely underexplored. This paper presents an MDD-based approach to support the structured design and implementation of quantum systems. Our framework enables the automatic generation of quantum code for multiple QPLs, thereby enhancing development efficiency and consistency across heterogeneous quantum platforms. The effectiveness and practicality of our approach have been demonstrated through multiple case studies.

cs.SE↗

arXiv2025

QuanBench: Benchmarking Quantum Code Generation with Large Language Models

Large language models (LLMs) have demonstrated good performance in general code generation; however, their capabilities in quantum code generation remain insufficiently studied. This paper presents QuanBench, a benchmark for evaluating LLMs on quantum code generation. QuanBench includes 44 programming tasks that cover quantum algorithms, state preparation, gate decomposition, and quantum machine learning. Each task has an executable canonical solution and is evaluated by functional correctness (Pass@K) and quantum semantic equivalence (Process Fidelity). We evaluate several recent LLMs, including general-purpose and code-specialized models. The results show that current LLMs have limited capability in generating the correct quantum code, with overall accuracy below 40% and frequent semantic errors. We also analyze common failure cases, such as outdated API usage, circuit construction errors, and incorrect algorithm logic. QuanBench provides a basis for future work on improving quantum code generation with LLMs.

cs.SE↗