Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2610.00255

Testing and Verification of Quantum Compilers through Assurance Contracts and Evidence

Furqan Nasir, Muhammad Arif Shah, Iftikhar Alam

Published Sep 24, 2026• 0 citations
arXivHTMLPDF

Abstract

Quantum compiler assurance requires a semantic relation that matches the intended use and observations that can expose violations at the delivered interface. This critical integrative survey compares verified transformations, equivalence checking, differential and metamorphic testing, property-based testing, and evidence for assurance across revisions. A source catalogue and focused extraction matrix distinguish formal guarantees, reported empirical findings, analytical deductions, and proposed practice. A recorded coverage update and source-level selection decisions make the review auditable within its declared scope. Four documented failure cases connect conditional applicability, parameter association, termination, and phase conventions to method selection. A worked example involving layout metadata, parameter bindings, and ancillary qubits demonstrates why validating a circuit under a reconstructed interpretation can leave the delivered interface unchecked. An illustrative revision scenario then separates fault detection from change attribution. The resulting guidance specifies applicability, complementary observations, and treatment of inconclusive outcomes. Published bug counts, mutation results, and processing benchmarks support different claims and do not establish a common effectiveness ranking. The proposed regression architecture remains unevaluated as a complete system; its practical value requires controlled comparisons on independently adjudicated compiler-change events.

DOI
10.48550/arxiv.2610.00255

Related papers

Are We Testing the Wrong Quantum Bugs? A Study of Fault Representation Gaps in Quantum Software Testing

Asif Mohammed Saad, Ahsanul Ameen Sabit, Jonah Brandenburgh +3 more

Quantum software relies on compilers, intermediate representations, and execution frameworks that transform programs before execution. Faults in these components can change the behavior of otherwise correct quantum programs. Yet quantum testing techniques are often evaluated using mutation-generated faults and curated bug benchmarks. We investigate how well the faults represented by these artifacts reflect those encountered in modern quantum software. We audit four quantum mutation-testing tools and three curated bug benchmarks, and collect 410 verified bugs from ten quantum software repositories over two years. We classify faults from all three sources into a common taxonomy of 56 bug families and compare their representation across mutation operators, curated benchmarks, and recent real-world bugs. The mutation tools support 20 bug families, and curated benchmarks add 15 more. Yet only 56 of the 410 real-world bugs (13.7%) belong to families represented by either source; the remaining 354 (86.3%) belong to families absent from both. The largest unrepresented families concern compiler transformations (66 bugs), type handling (53), and input validation (47). Unlike local gate or statement changes, these faults often depend on intermediate representations, compiler pipelines, input types, or dependency versions. Existing mutation operators primarily modify circuits and program constructs, whereas many real-world faults arise in the compilers, representations, and framework interfaces that process them. Addressing this gap requires looking beyond circuit-level faults toward testing semantic preservation across compiler transformations, correctness at representation boundaries, and interactions between software components. Our study provides empirical evidence to guide fault models and benchmarks that capture these mechanisms and preserve the contexts needed to reproduce them.

arXiv:2610.22089•Oct 15, 2026•0 citations

Auditing Empirical Comparisons in Quantum Software

Boshuai Ye, Peng Liang, Maryam Tavassoli Sabzevari +1 more

Empirical quantum-software papers often report that one compiler, optimizer, backend, or ansatz outperforms another. Such comparisons are not properties of a tool alone: they can change with benchmark scope, circuit construction, compilation, sampling, backend or noise assumptions, optimizer choices, and resource budgets. Existing testing, benchmarking, and reproducibility methods help assess programs, tools, executions, and platforms, but they do not directly audit whether the reported comparison itself is supported by the evidence exposed in the source paper or accompanying materials. We present CLAIMSTAB-QC, a source-bounded framework for auditing empirical comparisons in quantum software. Given a reported comparison, the framework records the baselines, metric, relation, and admissible evidence; locks the comparison design before outcomes are computed; and reports either a scoped relation outcome or an explicit evidence boundary. For strict scalar-directional comparisons, the reported direction is classified as Sustained, Unresolved, or Reversed within the locked audit scope. We evaluate CLAIMSTAB-QC on 455 comparative claims from 119 quantum-software papers. The central finding is a materialization gap: 175 claims can be represented for audit planning, 79 become scalar-directional planning records, 53 yield lockable audit or diagnostic designs, and only 8 expose enough matched evidence to audit the original comparison without proxy reconstruction. These 8 records yield 2 Sustained, 4 Unresolved, and 2 Reversed outcomes. Controlled diagnostics over 24 benchmark-relevant comparisons further show that simpler checks can preserve apparent directions whose support weakens under locked audit designs.

arXiv:2607.00516•Jul 1, 2026•0 citations

Fault-Class-Matched Test Oracles for Output-Invisible Quantum Transpiler Regressions

Furqan Nasir, Arif Shah, Iftikhar Alam

Test oracles for quantum transpilers typically judge correctness by comparing compiled output against a reference: a statevector, a sampled distribution, or a unitary compared modulo global phase. A companion empirical study measures how often that choice fails. Roughly 28% of merged Qiskit transpiler bug-fixes (95% Wilson CI 19-40%) repair a fault that corrupts layout metadata, global phase, or run-to-run reproducibility while output stays correct: invisible to a black-box output-equivalence oracle by construction. This paper closes that gap with a fault-class-matched, layout-aware, width-tiered oracle family: a layout/permutation contract checker and a contract-level metamorphic relation (MR-1) for the metadata channel, a global-phase tracker for the phase channel, and a determinism runner for reproducibility. Verified from source on nine real, merged Qiskit transpiler regressions (three per channel), the output-equivalence oracle is blind throughout and the matched mechanism fires on every case. A 675-configuration sweep of the contract/metadata invariant finds no false positive. Synthetic mutant families confirm reliability at scale: 1.00 sensitivity and specificity across 36 mutants apiece for the contract/metadata and global-phase channels, and 1.00 sensitivity (95% CI 0.44-1.00) for reproducibility on the three circuits where the mutation is constructible. The contract checker costs two to six orders of magnitude less than a plain output check, the global-phase tracker is comparably cheap within its exact tier, and only the metamorphic relation carries a bounded cost. Ported natively to pytket/tket, the global-phase mechanism transfers cleanly, an identical 1.00/1.00 result with phases recovered to double-precision accuracy, evidence against a Qiskit-specific artifact.

cs.SECross-listedarXiv:2609.24230•Sep 22, 2026•0 citations

Toward Circuit-Aware Mutation Testing for Quantum Programs: Exact Visibility and Execution Planning

Andriy Miranskyy, Jose Campos

Mutation testing assesses test suites by introducing program changes and checking whether tests detect them. In quantum programs, a surviving mutant may leave program behavior unchanged, produce a change hidden by the chosen input or measurement, or remain undetected because statistical evidence is insufficient. We develop a circuit-aware framework to distinguish these causes and guide execution planning and test changes. The framework covers ideal, noiseless programs and mutations that replace one gate or subcircuit. The method traces how a mutation can affect measured outputs and combines established mathematical checks with statistical estimates. For supported cases, we establish conditions under which a test cannot reveal a mutation and exact formulas for its effect when the required state information is available. Under stated assumptions, we bound the mutation score while retaining surviving and unresolved mutants, and identify a restricted circuit family whose mutation effects admit efficient classical classification. The deliverables include a decision procedure, mathematical guarantees, worked examples of test changes and their implementation requirements, and a small-circuit reference implementation for differential expectation tests. These results help testers decide what to execute, what to change, and what remains unknown. The evidence is limited to proofs and executable examples under the ideal model.

cs.SECross-listedarXiv:2610.36976•Oct 28, 2026•0 citations

What Output-Equivalence Oracles Miss: An Empirical Study of Equivalence-Invisible Bug Fixes in Quantum Transpilers

Furqan Nasir, Arif Shah, Iftikhar Alam

Quantum compilers face the test oracle problem, judged by an output-equivalence oracle: the compiled circuit must compute the same unitary as the original, modulo global phase and a qubit-layout permutation. This oracle, by construction, checks only that semantic map, not the circuit's own layout, permutation, or phase records: a defect there, or in a fixed-seed run's determinism, can pass unseen though the record is public. This empirical software engineering study of quantum transpiler correctness uses repository mining to measure how often this happens in real merged compiler fixes: a systematically identified corpus of Qiskit transpiler bug-fixes, classified by an independently dual-coded, source-validated fault-manifestation taxonomy. Nineteen of 68 fixes (28%, 95% Wilson CI 19-40%) repair faults invisible to this equivalence screen, even one augmented with compilation-validity, circuit-quality, and performance checks, and an extended 104-fix corpus over a wider window holds at the same rate with a tighter interval (29/104, 27.9%, CI 20-37%). A conservative floor remains even restricted to the one unconditionally equivalence-invisible channel (a corrupted layout or permutation record): 10 of 68 fixes (15%, CI 8-25%) beneath the 28% headline. The gap is not Qiskit-specific: it replicates in tket (7/21, 33%), with Cirq smaller but consistent. We detected no systematic differences on five inexpensive PR-level characteristics (19 vs 49, underpowered alone; the extended 29-vs-75 corpus tightens every interval toward zero). This class dominates the invisible set, concentrating at representation-boundary crossings. We release the corpus, codebook, and coding artifacts for quantum software testing research. Here we only measure it.

quant-pharXiv:2609.13839•Sep 15, 2026•0 citations

Two Undecided Predicates: Compilation Equivalence and the Sampling Boundary in Hybrid Quantum Runtime Governance

Paweł Bański, Sergiusz Sobieski

Willis (2026) argues that a recursively self-improving system may increase its effective quantum capability without acquiring additional hardware, and that the resulting hybrid classical-quantum execution path becomes progressively harder to characterise exhaustively. The proposed response abandons exhaustive reconstruction as an assurance objective and instead requires that specified properties hold before computation is permitted to affect consequential state, with five quantum execution controls layered beneath substrate-independent constitutional invariants. This paper accepts that architecture and contests two of its load-bearing predicates. The compilation equivalence predicate. GovernanceEquivalent(C(a), C(e)) carries the entire compilation-integrity argument and is left undefined. It cannot be read as semantic equivalence: deciding circuit equivalence is QMA-complete (Janzing, Wocjan & Beth, 2005), and remains so for the shallow circuits typical of transpiled output, while semantic sameness is in any case the wrong target given what transpilation exists to do. The predicate must therefore be evaluated relative to a declared set of governance-relevant properties. That set is itself a governance object, and under recursive self-improvement it is reachable through the toolchain. An attack follows in which a compilation change justified purely on performance grounds renders a governance-relevant property unmeasurable over the executed representation, so that the permit gate continues to evaluate correctly over a test that no longer discriminates. Traceability of the executed artefact to the authorised one does not prevent this, because traceability and property preservation come apart precisely when a transformation is faithful in derivation and lossy in representation. The sampling boundary. The authorised shot count is specified as a ceiling. A ceiling bounds resource consumption; it does not bound evidentiary resolution, which varies in the same direction. Admissibility evaluated on a point estimate is therefore unsound under an adversarial or merely cost-optimising choice of sample size, and error mitigation supplies a second route that widens the uncertainty region while appearing to improve result quality. Evaluating admissibility over a confidence region rather than a point estimate is sound, imposes the necessary floor implicitly, and fails closed without requiring a separately specified minimum. An authorised sequential-sampling rule is a second sound form, subject to the condition that the stopping rule be fixed prior to sampling. Composition. The two results are not independent. The repair proposed for the second introduces a parameter that is vulnerable to the first, and the properties governing sampling can themselves be attenuated out of the property set. Sound sampling governance presupposes governed property-set membership. General form. Both attacks share a shape: an invariant is enforceable only to the extent that the instrument deciding it — its property set, tolerance, confidence level, sample size, or measurability assumption — is unreachable from inside the system it constrains. Under recursive self-improvement there is always gradient in those parameters, because they trade against latency, cost and throughput, which are the objectives the recursion optimises. No adversarial disposition is required. The paper closes by applying its own criterion reflexively. A response whose complaint is that declarations are mistaken for proof cannot end with declarations and leave the matter there. A governance requirement is structural when its violation is observable without relying on the cooperation of the governed system, and declarative when it is not; three of the four requirements proposed here are organisational by that test, and one is not. This work continues the author's earlier treatment of trajectory-level governance and the Constitutional Failure Boundary methodology (Zenodo 10.5281/zenodo.18980403) and of admissibility operators and bounded reachability in probabilistic decision systems (Zenodo 10.5281/zenodo.20057043), extended here from classical to hybrid quantum execution. No implementation is described and none should be inferred. Attribution: the counterfactual authorisation test adapted in §3.6 was proposed by R. Muro. The Layer 3 / Layer 1 redefinition formulation in §3.5 and the authorised sequential-sampling rule in §4.4 are J. M. Willis's, offered in public response to an earlier and shorter statement of these arguments.

•Sep 11, 2026•0 citations
Quantum compiler assurance requires a semantic relation that matches the intended use and observations that can expose violations at the delivered interface. This critical integrative survey compares verified transformations, equivalence checking, differential and metamorphic testing, property-based testing, and evidence for assurance across revisions. A source catalogue and focused extraction matrix distinguish formal guarantees, reported empirical findings, analytical deductions, and proposed practice. A recorded coverage update and source-level selection decisions make the review auditable within its declared scope. Four documented failure cases connect conditional applicability, parameter association, termination, and phase conventions to method selection. A worked example involving layout metadata, parameter bindings, and ancillary qubits demonstrates why validating a circuit under a reconstructed interpretation can leave the delivered interface unchecked. An illustrative revision scenario then separates fault detection from change attribution. The resulting guidance specifies applicability, complementary observations, and treatment of inconclusive outcomes. Published bug counts, mutation results, and processing benchmarks support different claims and do not establish a common effectiveness ranking. The proposed regression architecture remains unevaluated as a complete system; its practical value requires controlled comparisons on independently adjudicated compiler-change events.
Quantum software relies on compilers, intermediate representations, and execution frameworks that transform programs before execution. Faults in these components can change the behavior of otherwise correct quantum programs. Yet quantum testing techniques are often evaluated using mutation-generated faults and curated bug benchmarks. We investigate how well the faults represented by these artifacts reflect those encountered in modern quantum software. We audit four quantum mutation-testing tools and three curated bug benchmarks, and collect 410 verified bugs from ten quantum software repositories over two years. We classify faults from all three sources into a common taxonomy of 56 bug families and compare their representation across mutation operators, curated benchmarks, and recent real-world bugs. The mutation tools support 20 bug families, and curated benchmarks add 15 more. Yet only 56 of the 410 real-world bugs (13.7%) belong to families represented by either source; the remaining 354 (86.3%) belong to families absent from both. The largest unrepresented families concern compiler transformations (66 bugs), type handling (53), and input validation (47). Unlike local gate or statement changes, these faults often depend on intermediate representations, compiler pipelines, input types, or dependency versions. Existing mutation operators primarily modify circuits and program constructs, whereas many real-world faults arise in the compilers, representations, and framework interfaces that process them. Addressing this gap requires looking beyond circuit-level faults toward testing semantic preservation across compiler transformations, correctness at representation boundaries, and interactions between software components. Our study provides empirical evidence to guide fault models and benchmarks that capture these mechanisms and preserve the contexts needed to reproduce them.
Empirical quantum-software papers often report that one compiler, optimizer, backend, or ansatz outperforms another. Such comparisons are not properties of a tool alone: they can change with benchmark scope, circuit construction, compilation, sampling, backend or noise assumptions, optimizer choices, and resource budgets. Existing testing, benchmarking, and reproducibility methods help assess programs, tools, executions, and platforms, but they do not directly audit whether the reported comparison itself is supported by the evidence exposed in the source paper or accompanying materials. We present CLAIMSTAB-QC, a source-bounded framework for auditing empirical comparisons in quantum software. Given a reported comparison, the framework records the baselines, metric, relation, and admissible evidence; locks the comparison design before outcomes are computed; and reports either a scoped relation outcome or an explicit evidence boundary. For strict scalar-directional comparisons, the reported direction is classified as Sustained, Unresolved, or Reversed within the locked audit scope. We evaluate CLAIMSTAB-QC on 455 comparative claims from 119 quantum-software papers. The central finding is a materialization gap: 175 claims can be represented for audit planning, 79 become scalar-directional planning records, 53 yield lockable audit or diagnostic designs, and only 8 expose enough matched evidence to audit the original comparison without proxy reconstruction. These 8 records yield 2 Sustained, 4 Unresolved, and 2 Reversed outcomes. Controlled diagnostics over 24 benchmark-relevant comparisons further show that simpler checks can preserve apparent directions whose support weakens under locked audit designs.
Test oracles for quantum transpilers typically judge correctness by comparing compiled output against a reference: a statevector, a sampled distribution, or a unitary compared modulo global phase. A companion empirical study measures how often that choice fails. Roughly 28% of merged Qiskit transpiler bug-fixes (95% Wilson CI 19-40%) repair a fault that corrupts layout metadata, global phase, or run-to-run reproducibility while output stays correct: invisible to a black-box output-equivalence oracle by construction. This paper closes that gap with a fault-class-matched, layout-aware, width-tiered oracle family: a layout/permutation contract checker and a contract-level metamorphic relation (MR-1) for the metadata channel, a global-phase tracker for the phase channel, and a determinism runner for reproducibility. Verified from source on nine real, merged Qiskit transpiler regressions (three per channel), the output-equivalence oracle is blind throughout and the matched mechanism fires on every case. A 675-configuration sweep of the contract/metadata invariant finds no false positive. Synthetic mutant families confirm reliability at scale: 1.00 sensitivity and specificity across 36 mutants apiece for the contract/metadata and global-phase channels, and 1.00 sensitivity (95% CI 0.44-1.00) for reproducibility on the three circuits where the mutation is constructible. The contract checker costs two to six orders of magnitude less than a plain output check, the global-phase tracker is comparably cheap within its exact tier, and only the metamorphic relation carries a bounded cost. Ported natively to pytket/tket, the global-phase mechanism transfers cleanly, an identical 1.00/1.00 result with phases recovered to double-precision accuracy, evidence against a Qiskit-specific artifact.
Mutation testing assesses test suites by introducing program changes and checking whether tests detect them. In quantum programs, a surviving mutant may leave program behavior unchanged, produce a change hidden by the chosen input or measurement, or remain undetected because statistical evidence is insufficient. We develop a circuit-aware framework to distinguish these causes and guide execution planning and test changes. The framework covers ideal, noiseless programs and mutations that replace one gate or subcircuit. The method traces how a mutation can affect measured outputs and combines established mathematical checks with statistical estimates. For supported cases, we establish conditions under which a test cannot reveal a mutation and exact formulas for its effect when the required state information is available. Under stated assumptions, we bound the mutation score while retaining surviving and unresolved mutants, and identify a restricted circuit family whose mutation effects admit efficient classical classification. The deliverables include a decision procedure, mathematical guarantees, worked examples of test changes and their implementation requirements, and a small-circuit reference implementation for differential expectation tests. These results help testers decide what to execute, what to change, and what remains unknown. The evidence is limited to proofs and executable examples under the ideal model.
Quantum compilers face the test oracle problem, judged by an output-equivalence oracle: the compiled circuit must compute the same unitary as the original, modulo global phase and a qubit-layout permutation. This oracle, by construction, checks only that semantic map, not the circuit's own layout, permutation, or phase records: a defect there, or in a fixed-seed run's determinism, can pass unseen though the record is public. This empirical software engineering study of quantum transpiler correctness uses repository mining to measure how often this happens in real merged compiler fixes: a systematically identified corpus of Qiskit transpiler bug-fixes, classified by an independently dual-coded, source-validated fault-manifestation taxonomy. Nineteen of 68 fixes (28%, 95% Wilson CI 19-40%) repair faults invisible to this equivalence screen, even one augmented with compilation-validity, circuit-quality, and performance checks, and an extended 104-fix corpus over a wider window holds at the same rate with a tighter interval (29/104, 27.9%, CI 20-37%). A conservative floor remains even restricted to the one unconditionally equivalence-invisible channel (a corrupted layout or permutation record): 10 of 68 fixes (15%, CI 8-25%) beneath the 28% headline. The gap is not Qiskit-specific: it replicates in tket (7/21, 33%), with Cirq smaller but consistent. We detected no systematic differences on five inexpensive PR-level characteristics (19 vs 49, underpowered alone; the extended 29-vs-75 corpus tightens every interval toward zero). This class dominates the invisible set, concentrating at representation-boundary crossings. We release the corpus, codebook, and coding artifacts for quantum software testing research. Here we only measure it.
Willis (2026) argues that a recursively self-improving system may increase its effective quantum capability without acquiring additional hardware, and that the resulting hybrid classical-quantum execution path becomes progressively harder to characterise exhaustively. The proposed response abandons exhaustive reconstruction as an assurance objective and instead requires that specified properties hold before computation is permitted to affect consequential state, with five quantum execution controls layered beneath substrate-independent constitutional invariants. This paper accepts that architecture and contests two of its load-bearing predicates. The compilation equivalence predicate. GovernanceEquivalent(C(a), C(e)) carries the entire compilation-integrity argument and is left undefined. It cannot be read as semantic equivalence: deciding circuit equivalence is QMA-complete (Janzing, Wocjan & Beth, 2005), and remains so for the shallow circuits typical of transpiled output, while semantic sameness is in any case the wrong target given what transpilation exists to do. The predicate must therefore be evaluated relative to a declared set of governance-relevant properties. That set is itself a governance object, and under recursive self-improvement it is reachable through the toolchain. An attack follows in which a compilation change justified purely on performance grounds renders a governance-relevant property unmeasurable over the executed representation, so that the permit gate continues to evaluate correctly over a test that no longer discriminates. Traceability of the executed artefact to the authorised one does not prevent this, because traceability and property preservation come apart precisely when a transformation is faithful in derivation and lossy in representation. The sampling boundary. The authorised shot count is specified as a ceiling. A ceiling bounds resource consumption; it does not bound evidentiary resolution, which varies in the same direction. Admissibility evaluated on a point estimate is therefore unsound under an adversarial or merely cost-optimising choice of sample size, and error mitigation supplies a second route that widens the uncertainty region while appearing to improve result quality. Evaluating admissibility over a confidence region rather than a point estimate is sound, imposes the necessary floor implicitly, and fails closed without requiring a separately specified minimum. An authorised sequential-sampling rule is a second sound form, subject to the condition that the stopping rule be fixed prior to sampling. Composition. The two results are not independent. The repair proposed for the second introduces a parameter that is vulnerable to the first, and the properties governing sampling can themselves be attenuated out of the property set. Sound sampling governance presupposes governed property-set membership. General form. Both attacks share a shape: an invariant is enforceable only to the extent that the instrument deciding it — its property set, tolerance, confidence level, sample size, or measurability assumption — is unreachable from inside the system it constrains. Under recursive self-improvement there is always gradient in those parameters, because they trade against latency, cost and throughput, which are the objectives the recursion optimises. No adversarial disposition is required. The paper closes by applying its own criterion reflexively. A response whose complaint is that declarations are mistaken for proof cannot end with declarations and leave the matter there. A governance requirement is structural when its violation is observable without relying on the cooperation of the governed system, and declarative when it is not; three of the four requirements proposed here are organisational by that test, and one is not. This work continues the author's earlier treatment of trajectory-level governance and the Constitutional Failure Boundary methodology (Zenodo 10.5281/zenodo.18980403) and of admissibility operators and bounded reachability in probabilistic decision systems (Zenodo 10.5281/zenodo.20057043), extended here from classical to hybrid quantum execution. No implementation is described and none should be inferred. Attribution: the counterfactual authorisation test adapted in §3.6 was proposed by R. Muro. The Layer 3 / Layer 1 redefinition formulation in §3.5 and the authorised sequential-sampling rule in §4.4 are J. M. Willis's, offered in public response to an earlier and shorter statement of these arguments.