Bayesian Sequential Verification for Budget-Aware Quantum Program Testing Lei Zhang
arXiv:2605.15601v1 [cs.SE] 15 May 2026
Department of Information Systems University of Maryland, Baltimore County Maryland, USA [email protected]
Abstract—Quantum programs often produce probability distributions rather than deterministic outputs, making verification inherently statistical and increasingly costly on real hardware. In practice, developers still frequently rely on testing with fixed shot budgets on simulators, which are simple but time-consuming and poorly suited to noisy backends. What is missing is a verification approach that is both statistically explicit and budget-aware. This paper formulates Bayesian sequential verification as a reference-based Bayesian hypothesis testing workflow in which priors are derived from explicit reference sources, such as finiteshot reference runs or ideal/statevector-based computation, and verification decisions are updated batch by batch as measurement evidence accumulates. This approach is evaluated in Qiskit on two complementary workloads: Bell-state and QAOA-MaxCut. Across both case studies, the results show that Bayesian sequential verification can substantially reduce measurement costs compared to fixedbudget baselines when the success probability of the program exceeds the target threshold. The findings position Bayesian sequential verification as a practical verification workflow for quantum programs. The approach provides a foundation for future quantum continuousintegration pipelines that require reliable, budget-aware pass/fail decisions and motivates validation on real quantum hardware. Index Terms—Bayesian hypothesis testing, quantum software engineering, quantum software testing
I. I NTRODUCTION Quantum programs increasingly produce probability distributions rather than single deterministic outputs, relying on repeated measurement to estimate performance-relevant properties [1]–[3]. Unlike classical probabilistic programs, they do not expose an internal state that can be deterministically checked at runtime [4], [5]; instead, correctness must be inferred from stochastic outcomes whose distribution depends on quantum hardware noise, compilation choices, and device drift [6], [7]. As a result, verification is inherently distributional and resource constrained: each additional shot consumes real hardware budget (e.g., IBM quantum resources can cost $96 USD per minute) [8], outcomes may shift over time, and practically meaningful criteria are often task-level (e.g., success probability over a set of high-quality solutions) rather than exact functional equivalence on individual inputs. Despite this, current practice often relies on fixed and adhoc shot budgets (e.g., 10k shots per circuit) [9]. Such fixedshot testing is easy to apply, but statistically inefficient. If the observed behavior of the program (e.g., its success probability)
is clearly above the target threshold, a large fixed budget can waste shots. Otherwise, the same budget may be insufficient because sampling uncertainty can be too large to support a confident decision. To address these limitations, this paper formulate a Bayesian sequential verification approach for quantum programs: a reference-based Bayesian Hypothesis Testing (BHT) [10] workflow in which the prior is derived from an explicit reference source (e.g., shot-derived from a noiseless simulator, or a statevector distribution), while verification decisions are updated batch by batch as shots are collected rather than committed to a fixed budget in advance. Concretely, this paper casts verification as deciding whether a backend’s property success probability exceeds a target threshold, and we implement a sequential Bayesian procedure that updates a Beta posterior from batched measurements and verifies once a conservative lower credible bound (LCB) crosses the target. To summarize, this approach encodes prior knowledge from simulation or prior runs, quantifies uncertainty under finite shots, and expresses verification outcomes as explicit evidence thresholds. These properties make BHT a promising foundation for future quantum continuous-integration (CI) settings, where verification must be both budget-aware and statistically defensible. To validate the BHT workflow, this paper implements a Qiskit-based [11] harness and applies it on two case studies: (i) Bell-state [12] correlation verification in complementary Z/X measurement bases [13], and (ii) the Quantum Approximate Optimization Algorithm (QAOA) [14] for combinatorial optimization (e.g., MaxCut [15]) using a Top-K success predicate under ideal and noisy execution models [16]. In both cases, we also compare BHT against a matched fixed-budget baseline to assess whether the observed shot savings persist beyond caprelative comparisons. The contributions of this paper are: (i) formulating a Bayesian sequential verification procedure for quantum programs under finite shot budgets; (ii) evaluating this workflow on two complementary Qiskit case studies across multiple IBM fake backends with noise, including matched fixedbudget baseline [17], and 3) releasing the artifacts publicly on Zenodo for reproduction and reuse at doi:10.5281/zenodo. 18341209. Note that this paper does not claim a new Bayesian sta-
tistical method; rather, it operationalize BHT as a reusable verification workflow for quantum programs under finite shot budgets. Overall, this research aims to make quantum regression checks more budget-aware and statistically rigorous by replacing fixed-shot testing with explicit posterior guarantees. Moreover, the case studies are initial evidence of feasibility for future CI-driven quantum regression testing. The remainder of this paper is organized as follows. Section II motivates Bayesian sequential verification in the context of quantum-program testing. Section III presents the referencebased BHT workflow, including prior construction, posterior updates, and stopping rules. Section IV evaluates the approach on Bell-state verification, and Section V studies a more challenging QAOA Top-K verification task. Section VI discusses the baseline comparison and summarizes lessons from the matched fixed-budget baselines. Finally, Sections VII and VIII discuss threats to validity and conclude with directions for future work. II. BACKGROUND AND M OTIVATION In classical verification, Bayesian statistical model checking and sequential decision procedures provide principled mechanisms to accept, reject, or continue testing as observations accrue [18], [19]. However, many classical applications assume relatively stable observation processes and specifications evaluated over deterministic traces or well-controlled stochastic models. Quantum software pushes these assumptions: observable behavior is sample-based, hardware is costly, and nonstationary noise can cause statistically meaningful variation even when the source code is unchanged. Recent work has begun to characterize noise and detect flakiness in quantum programs, underscoring the need for verification methods that are distribution-aware and can separate genuine regressions from hardware-induced variance [6], [7]. Moreover, Miranskyy’s work [20] develops a unified framework for estimating the number of measurements required for quantum program verification, analyzes inverse, swap, and chi-square tests, and studies how verification budgets scale at the program level. Our work differs from the above literature, unlike estimating the measurement cost of fixed testing procedures, we formulate a sequential Bayesian decision process that can stop early once sufficient posterior evidence has accumulated. In quantum advantage validation—including boson sampling [21] and random-circuit-style experiments [22]— Bayesian hypothesis testing and likelihood-based model comparison have been used to contrast a target quantum model against classical or adversarial alternatives, reporting evidential measures such as posterior odds or Bayes factors [23], [24]. These efforts demonstrate two properties that are particularly relevant to near-term quantum computing: (i) evidence can be accumulated sequentially as samples arrive, and (ii) prior knowledge can be represented explicitly rather than remaining informal. Our setting differs from prior quantum-validation use cases in both goal and workflow. This paper focuses on quantum
Bayesian Sequential Verification Workflow Reference Source Simulator / statevector / baseline run
Construct Prior
Execute Program on Backend
Encode prior belief about expected success probability
Collect evidence in small batches of shots
Update Posterior Combine prior knowledge with observed evidence
FAIL Budget exhausted n_stop = n_max
LCB ≥ τ ?
yes
PASS (early stop)
no
budget limit
Continue next batch
Fig. 1. Overall illustration of the Bayesian sequential verification workflow.
program verification for software engineering: enabling repeatable checks such as regression testing across runs, backends, transpiler settings, and library updates, rather than demonstrating quantum advantage. In practice, quantum developers often have usable reference information, such as small-instance simulations used during unit testing, previously certified baselines from nightly builds, and historical test artifacts collected by CI pipelines. Yet this reference information is rarely integrated into test decisions in a statistically explicit and configurable way. Our contribution is to treat these artifacts as explicit reference sources for prior construction and to show how Bayesian sequential verification can use them to guide sampleefficient regression checks while preserving conservative decision guarantees. III. BAYESIAN S EQUENTIAL V ERIFICATION FOR Q UANTUM P ROGRAMS A quantum program (circuit) P executed on a backend B induces an unknown outcome distribution pB over a discrete space Y (e.g., bitstrings). Each execution yields an outcome y ∈ Y. This paper assumes that, within a single run, outcomes are conditionally i.i.d. given pB and that pB is stationary over the shots collected in that run.1 Both case studies instantiate verification as a property-based Bernoulli predicate ϕ : Y → {0, 1} (success/failure), inducing an unknown backend success probability θ := Pry∼pB (ϕ(y) = 1). As shown in Figure 1, this paper performs Bayesian sequential verification by (i) initializing a prior for θ from a reference success rate µ0 and prior strength s, (ii) updating the posterior as shots are collected in batches, and (iii) declaring PASS once a conservative one-sided LCB meets the target threshold under a stopping rule. A. Prior construction In this paper, prior information supports two reference sources, i.e., shot-derived priors and computed priors. In both cases, we denote the reference success rate by µ0 . 1 We use independent seeds and short runs to reduce the risk of long-term drift; handling drift explicitly is outside the scope of this paper.
Algorithm 1 Sequential Bayesian verification for a property ϕ Inputs: program P , backend B, outcome space Y specification ϕ : Y → {0, 1} prior source R (shot-derived or analytic/statevectorderived) prior strength s > 0, targets (τ, δ), batch size b shot cap nmax , minimum-shot gate nmin , pass-streak requirement r Outputs: decision PASS/FAIL, stopping time nstop 1: Compute reference success rate µ0 ← PrR (ϕ(y) = 1) 2: Set prior parameters: α0 ← 1 + sµ0 , β0 ← 1 + s(1 − µ0 ) 3: Initialize n ← 0, k ← 0, streak ← 0 4: while n < nmax do 5: Execute PPon B for b shots and obtain outcomes y1:b b 6: k ← k + j=1 ϕ(yj ); n ← n + b 7: Compute posterior lower bound LCB ← BetaInv δ; α0 + k, β0 + n − k 8: if n ≥ nmin and LCB ≥ τ then 9: streak ← streak + 1 10: if streak ≥ r then 11: return PASS, nstop ← n 12: end if 13: else 14: streak ← 0 15: end if 16: end while 17: return FAIL, nstop ← nmax
Shot-derived priors (empirical reference). When a measurement-driven reference workflow is preferred, we estimate the reference success rate from a noiseless or baseline backend Bref by running P for n0 shots: µ0 =
k0 , n0
k0 =
n0 X
(ref)
ϕ(yi
).
i=1
This is the approach used in the Bell-state case study (Section IV). Computed priors (analytic/statevector reference). When the reference success probability can be computed directly, we set X µ0 = Pr ϕ(y) = 1 = ϕ(y) pref (y), ref
y∈Y
which avoids additional Monte Carlo variance in the prior. This is the approach used in the QAOA case study (Section V). In either case, we model the success probability θ using a Beta prior, which is the conjugate prior for Bernoulli observations and enables closed-form posterior updates. We instantiate the prior as θ ∼ Beta(α0 , β0 ),
β0 = 1 + s (1 − µ0 ), (1) where µ0 is the reference success rate and s controls the prior strength. We interpret s as an equivalent prior sample size, so that the prior contributes s pseudo-observations centered at α0 = 1 + s µ0 ,
µ0 , regularizing early batches without dominating the posterior once hundreds to thousands of backend shots accumulate. Empirically, we set the prior strength to s = 20 in all experiments. B. Posterior updates Program P is executed on the target backend B in batches of size b. After batch t, let nt be the cumulative number of shots and kt the cumulative number of successes under ϕ. The posterior is θ | (kt , nt ) ∼ Beta(α0 + kt , β0 + nt − kt ).
(2)
This update can be performed online after each batch and directly supports the one-sided LCB used by the stopping rule in Section III-C. C. Decision rule and stopping policy Given a target threshold τ ∈ (0, 1] and tail probability δ, we compute a conservative one-sided LCB LCB1−δ (θ) = BetaInv δ; α0 + k, β0 + n − k . (3) After each batch, once the cumulative shots satisfy n ≥ nmin , we check whether LCB1−δ (θ) ≥ τ. This algorithm stops and outputs PASS at the earliest stopping time nstop for which this condition holds for r consecutive batch checks (the pass-streak requirement). If the shot cap nmax is reached before this occurs, the algorithm stops and outputs FAIL with nstop = nmax . D. Evaluation metrics The verifier is evaluated over repeated randomized runs (different seeds) to characterize both decision behavior and sample efficiency. For each configuration (backend B and threshold τ ), we execute R independent runs and report: 1) PASS rate, the fraction of runs that satisfy the stopping rule before reaching nmax ; 2) shot cost, the stopping time nstop (set to nmax for FAIL runs); and 3) dispersion, summarized by the interquartile range (IQR) of {nstop } reported as [Q1 , Q3 ]. E. Experimental settings Unless otherwise noted, both case studies instantiate Algorithm 1 with the same sequential verification policy: batch size b = 50, pass-streak requirement r = 2, and prior strength s = 20. For Bell-state verification, the shot cap is nmax = 2,000 and the minimum-shot gate is nmin = 200. For QAOA verification, the shot cap is nmax = 10,000 and the minimum-shot gate is nmin = 1,000. Thus, the two case studies differ only in the success predicate ϕ and in how the reference success rate µ0 is constructed: Bell uses a shotderived reference from a noiseless simulator, whereas QAOA uses a statevector-derived ideal reference.
TABLE I B ELL - STATE VERIFICATION ACROSS IBM FAKE BACKENDS USING A NOISELESS PRIOR (A E R S I M U L A T O R ). E ACH τ USES R=10 SEEDS ; PASS REQUIRES BOTH Z- AND X - BASIS CHECKS TO VERIFY WITHIN A SHOT CAP OF 2,000. T HIS TABLE REPORTS THE MEDIAN PER - RUN COST median(max(nZ , nX )) AND IQR [Q1 , Q3 ].
τ 0.85 0.88 0.90 0.92 0.94
PASS 10/10 10/10 8/10 0/10 0/10
FakeNairobiV2 Med. max-shots IQR 250 [250, 250] 400 [288, 488] 1175 [813, 1738] 2000 [2000, 2000] 2000 [2000, 2000]
PASS 10/10 10/10 10/10 10/10 3/10
FakeLimaV2 Med. max-shots IQR 250 [250, 250] 250 [250, 250] 325 [250, 400] 575 [250, 850] 2000 [2000, 2000]
IV. U SE C ASE 1: B ELL STATE (Z & X BASES ) Goal. This paper studies a 2-qubit circuit that prepares the Bell state √ Φ+ = (|00⟩ + |11⟩)/ 2 by applying a Hadamard gate to qubit 0 followed by a CNOT from qubit 0 to qubit 1. In the ideal setting, measurement in the computational (Z) basis yields only outcomes {00, 11} with equal probability: (Z)
Pideal = {00 : 0.5, 11 : 0.5}. In practice, noise can introduce (i) population errors that leak probability mass to {01, 10} and/or (ii) phase decoherence that preserves Z-basis correlations while degrading coherence. To detect both effects, the state is verified in two complementary measurement configurations: the Z basis (direct measurement after Bell-state preparation) and the X basis, implemented by applying H ⊗2 before measurement. For |Φ+ ⟩, the ideal Xbasis outcomes are again perfectly correlated, so only {00, 11} appear in the post-Hadamard measurement frame. Bayesian sequential verification (per basis). For each basis b ∈ {Z, X}, a Bernoulli success event is defined as observing a correlated outcome: Success in Z : y ∈ {00, 11}, Success in X : y ∈ {00, 11}
after applying H ⊗2 .
The prior is derived from shot-based estimates on a noiseless AerSimulator (2,000 shots per basis), yielding reference success rates µZ and µX . The posterior is then updated sequentially using measurements collected from noisy IBM fake backends, with a per-run shot cap of nmax = 2,000. Thus, the testing procedure uses a fixed budget as an upper bound, while allowing early stopping when sufficient evidence is obtained. Results and interpretation. Table I reports Bell-state verification outcomes across three IBM fake backends for a sweep of thresholds τ (10 seeds per setting). The results show a clear tradeoff: moderate thresholds τ typically verify with significantly fewer than 2,000 shots, whereas stricter thresholds τ increase both the median shot cost (sometimes running to the maximum number of shots) and its variability. We highlight two observations. First, when the observed success probability θ is well above the threshold τ , the posterior quickly accumulates strong evidence, so the test can
PASS 10/10 10/10 10/10 10/10 0/10
FakeManilaV2 Med. max-shots IQR 250 [250, 250] 250 [250, 250] 350 [250, 400] 825 [350, 1250] 2000 [2000, 2000]
stop early. For example, at τ = 0.85, all three backends achieve PASS = 10/10 with a median of only 250 maxshots and a tight IQR [250, 250], corresponding to an 87.5% shot reduction relative to the fixed budget. Second, when the backend is near the decision boundary—often dominated by the more demanding coherence check in the X basis— the method becomes conservative, requiring more shots or returning a budget-limited FAIL. For example, at τ = 0.92, FakeNairobiV2 fails in all runs (0/10) and reaches the shot cap, whereas FakeLimaV2 and FakeManilaV2 still pass (10/10) with shot reductions of 71.25% and 58.75%, respectively; their wider IQRs reflect increased variability near the threshold. These results suggest that practical regression workflows may need backend-specific calibration of τ to balance assurance against test cost. V. U SE C ASE 2: QAOA (T OP -K) Goal. This paper studies an 8-qubit QAOA-based MaxCut instance and verifies whether the circuit produces high-quality solutions with sufficient frequency. Rather than verifying a single bitstring, we verify Top-K success: the probability mass assigned to a target set SK containing the K highest-scoring bitstrings under the objective. This metric is aligned with nearterm optimization practice, where recovering any of several high-quality solutions is acceptable [25]. Top-K success event. Let z ∈ {0, 1}n denote a measured bitstring and let C(z) be its MaxCut value. We define the success set SK as the K highest-scoring bitstrings under the ideal noiseless model and use the Bernoulli success predicate ϕ(z) = I[z ∈ SK ]. The corresponding reference success probability is µ0 = Pr (z ∈ SK ), ideal
which is computed directly from the ideal distribution and use to instantiate the Beta prior in Eq. 1. A fixed MaxCut ring instance is used with n = 8 vertices and edge set {(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 0)}, with QAOA depth p = 1. We set K = 5 and select the angles (γ ⋆ , β ⋆ ) by a coarse ideal-statevector grid search over γ ∈ linspace(0.1, 2.9, 15) and β ∈ linspace(0.1, 1.5, 15), yielding (γ ⋆ , β ⋆ ) = (2.300, 1.200). For this instance
TABLE II QAOA T OP -K VERIFICATION ACROSS IBM BACKENDS USING AN IDEAL ( STATEVECTOR - DERIVED ) PRIOR µ0 AND A POSTERIOR - ONLY LCB STOPPING RULE . E ACH τ USES R=10 SEEDS . T HIS TABLE REPORTS MEDIAN STOPPING SHOTS AND IQR [Q1 , Q3 ]; THE SHOT CAP IS nmax = 10,000.
τ 0.60 0.70 0.80 0.85 0.90 0.95
PASS 10/10 10/10 10/10 10/10 10/10 8/10
AerSimulator Med. shots IQR 150 [100, 188] 225 [112, 375] 375 [212, 538] 450 [262, 1138] 525 [375, 1875] 2350 [662, 7100]
PASS 9/10 7/10 5/10 2/10 2/10 2/10
FakeBrooklynV2 Med. shots IQR 650 [250, 3850] 4600 [1138, 9962] 9275 [2750, 10000] 10000 [10000, 10000] 10000 [10000, 10000] 10000 [10000, 10000]
and parameter setting, the ideal Top-5 success mass is µ0 ≈ 0.1813. Then, Algorithm 1 is applied on three target backends: AerSimulator (noiseless baseline), FakeBrooklynV2, and FakeKolkataV2. For each (τ, backend), we run R=10 seeds and report PASS rate and the distribution of stopping shots. Results and interpretation. Table II reports sequential Top5 verification outcomes. On AerSimulator, all runs verify for τ ≤ 0.90 (PASS rate = 1.00) with only a few hundred shots (median 150– 525). At τ = 0.95, verification becomes less stable: PASS rate drops to 0.80, and shot cost increases sharply (median 2,350, IQR [662, 7,100]), indicating a near-threshold case. On noisy FakeBrooklynV2 and FakeKolkataV2, verification is already costly at τ = 0.70 (PASS 7/10 and 6/10, respectively), with medians in the 4,000–5,000-shot range and wide variability. For τ ≥ 0.80, most runs become budgetlimited at 10,000 shots, suggesting that the proposed algorithm does not have enough evidence to pass, even after using the full budget. Compared with the Bell-state case, QAOA verification is significantly more noise-sensitive: under hardware-realistic noise, both PASS probability and stopping-time stability degrade rapidly as τ increases. This reflects the fact that Top-K success is a lower-probability event than Bell-state correlation, making the posterior lower bound slower to separate from the target under noise. These findings suggest that future Top-K regression policies may benefit from more robust predicate design (e.g., larger K), multi-threshold stopping rules, and backend-specific calibration. VI. D ISCUSSION Table III compares BHT against a matched fixed-budget baseline in both workloads. In Bell-state verification, the baseline evaluates the same basis-specific Bernoulli event— observing a correlated outcome—and the same confidence target, but makes its decision only at the fixed budget. In QAOA verification, the comparison is also matched at the level of the success event, confidence level, and decision target: both methods test whether LCB0.975 (θ) ≥ τ µ0 , where θ is the Top-K success probability, µ0 ≈ 0.1813 is the ideal TopK success mass, and the fixed baseline evaluates this rule only at nmax = 10,000. For QAOA, a fixed 8-node ring
PASS 10/10 6/10 2/10 2/10 1/10 1/10
FakeKolkataV2 Med. shots IQR 1150 [612, 4538] 4050 [1475, 10000] 10000 [10000, 10000] 10000 [10000, 10000] 10000 [10000, 10000] 10000 [10000, 10000]
MaxCut instance is used with n = 8, QAOA depth p = 1, K = 5, batch size b = 50, pass-streak requirement r = 2, prior strength s = 20, minimum-shot gate nmin = 1,000, and R = 10 seeds per threshold. The QAOA angles are selected once by coarse ideal-statevector grid search, yielding (γ ⋆ , β ⋆ ) = (2.300, 1.200). The baseline comparison shows that the advantage of the proposed method is not that BHT stops earlier than a configured shot cap, but that it can preserve a clear confidence rule. The sequential rule often achieves the same or higher PASS count as the fixed-budget baseline while using fewer shots. For example, this pattern is visible in Bell-state verification at moderate thresholds such as τ = 0.85 and τ = 0.88, where all three backends achieve identical PASS counts under both methods but BHT saves roughly 1,600–1,750 shots. A similar behavior appears in QAOA at lower thresholds: on FakeBrooklynV2 at τ = 0.70, e.g., BHT improves PASS from 5/10 to 7/10 while saving a median of 5,400 shots relative to the fixed-budget test. As the target threshold approaches the effective success probability under noise, posterior lower bounds tighten more slowly and both sequential and fixed-budget rules become increasingly conservative. In Bell-state verification, this appears at thresholds such as τ = 0.92 and τ = 0.94, where savings can disappear on the more challenging backends. In QAOA, the effect is stronger because Top-K success is a substantially smaller-probability event than Bell-state correlation. The matched baseline confirms this behavior: BHT provides clear gains at τ = 0.60 and τ = 0.70, more modest gains at τ = 0.80, and no median-shot advantage once runs become budget-limited. As shown by the experiments and findings, the two case studies are complementary. Bell-state verification serves as a simple demonstration of the method: the success predicate is simple, and the ideal success probability is high. QAOA verification plays a different role as a stress test for the method, where early stopping remains effective and where noise pushes the problem into a near-threshold zone. These observations suggest a practical role for Bayesian sequential verification in future quantum CI workflows. When a system is well above specification, sequential verification can provide large-shot savings with little loss. When the system is near the decision boundary, however, both BHT and fixedbudget baselines become conservative, indicating the need
TABLE III BHT VS . MATCHED FIXED - BUDGET BASELINES ACROSS BOTH CASE STUDIES . F OR B ELL - STATE VERIFICATION , THE BASELINE IS A ONE - SIDED FIXED - BUDGET BINOMIAL LCB TEST USING THE SAME CORRELATED - OUTCOME SUCCESS EVENT AND THE SAME CONFIDENCE TARGET AS BHT. F OR QAOA VERIFICATION , THE BASELINE USES THE SAME SUCCESS EVENT, THE SAME CONFIDENCE TARGET, AND THE SAME SCALED DECISION TARGET AS BHT, I . E ., LCB0.975 (θ) ≥ τ µ0 , BUT EVALUATES THE RULE ONLY AT THE FIXED BUDGET. E ACH τ USES R=10 SEEDS . T HIS PAPER REPORTS BHT PASS COUNT, FIXED - BASELINE PASS COUNT, AND MEDIAN SHOT SAVING OF BHT RELATIVE TO THE FIXED - BUDGET BASELINE .
Bell-state verification τ
BHT PASS
0.85 0.88 0.90 0.92 0.94
10/10 10/10 8/10 0/10 0/10
FakeNairobiV2 Fixed PASS Med. saving 10/10 10/10 6/10 0/10 0/10
1750 1600 825 0 0
BHT PASS
FakeLimaV2 Fixed PASS Med. saving
10/10 10/10 10/10 10/10 3/10
10/10 10/10 10/10 10/10 2/10
1750 1750 1675 1425 0
BHT PASS 10/10 10/10 10/10 10/10 0/10
FakeManilaV2 Fixed PASS Med. saving 10/10 10/10 10/10 10/10 0/10
1750 1750 1650 1175 0
QAOA Top-K verification τ
BHT PASS
0.60 0.70 0.80 0.85 0.90 0.95
10/10 10/10 10/10 10/10 10/10 8/10
AerSimulator Fixed PASS Med. saving 10/10 10/10 10/10 10/10 10/10 7/10
9850 9775 9625 9550 9475 7650
FakeBrooklynV2 BHT PASS Fixed PASS Med. saving 9/10 7/10 5/10 2/10 2/10 2/10
for more robust mechanisms as suggested in Section V. The next step is to validate the same workflow on real quantum hardware, where calibration drift and nonstationary behaviors may further affect stopping rules and BHT’s reliability. VII. T HREATS TO VALIDITY Internal validity is influenced by implementation choices such as batch size, minimum-shot gate, pass-streak requirement, prior strength, and shot cap. Although these settings are fixed and reported explicitly, different parameter choices may affect stopping behavior and PASS rates, especially near the decision boundary. In addition, the matched fixed-budget baseline is only one comparator and should not be interpreted as exhausting the space of possible sequential or frequentist alternatives. Construct validity is limited by the way correctness is operationalized in the two case studies. Both workloads reduce verification to a Bernoulli success predicate: correlated outcomes in Bell-state verification and Top-K success in QAOAMaxCut. These predicates are meaningful for the targeted tasks, but they do not capture all possible notions of correctness or quality. External validity is limited because our evaluation uses AerSimulator and IBM fake backends rather than real quantum hardware. This improves reproducibility and allows controlled study of noise-model effects, but real devices may introduce additional variability, including calibration drift, queue delays, and nonstationary noise. Due to the limited access and the high cost of quantum hardware, further verification on real backends will be addressed in future research with more external support.
8/10 5/10 2/10 0/10 0/10 0/10
9350 5400 725 0 0 0
BHT PASS 10/10 6/10 2/10 2/10 1/10 1/10
FakeKolkataV2 Fixed PASS Med. saving 9/10 3/10 0/10 0/10 0/10 0/10
8850 5950 0 0 0 0
Conclusion validity is limited by the scope of the empirical study. The paper provides a proof-of-concept design study rather than a comprehensive benchmark over all verification strategies. Accordingly, our conclusions about the benefits of BHT are strongest for the tested settings and workloads, and the observed savings should be interpreted relative to the reported shot budgets and matched baseline configuration. Further validation on real hardware and broader benchmark suites is needed before drawing stronger claims. VIII. C ONCLUSION AND F UTURE W ORK This paper presents Bayesian sequential verification as a practical workflow for quantum programs. Rather than relying on fixed-shot testing, the proposed approach uses reference-based priors, sequential posterior updates, and conservative one-sided LCB to make verification decisions under finite shot budgets. Across two complementary Qiskitbased case studies—Bell-state verification and QAOA Top-K verification—this paper shows that the same verification logic transfers across qualitatively different success predicates and remains competitive against matched fixed-budget baselines. Several directions remain for future work. First, prior selection and refresh should be systematized through lightweight prior management across repeated runs. Second, a variety of fault models could be explored when tests fail. Third, the same workflow should be validated on real quantum hardware. Together, these steps would move Bayesian sequential verification closer to reliable quantum software testing under tight measurement budgets. DATA AVAILABILITY The Python scripts and experimental results are available at doi:10.5281/zenodo.18341209.
R EFERENCES [1] J. Zhao, “Quantum software engineering: Landscapes and horizons,” arXiv preprint arXiv:2007.07047, 2020. [2] A. Miranskyy and L. Zhang, “On testing quantum programs,” in 2019 IEEE/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER). IEEE, 2019, pp. 57–60. [3] R. Abreu, S. Ali, P. Arcaini, J. Campos, M. Felderer, C. Gravel, F. Ishikawa, S. Klikovits, A. Miranskyy, M. Mousavi, M. Yamaguchi, L. Zhang, J. Zhao, and A. Mjeda, “Software testing in the quantum world,” 2026. [Online]. Available: https://arxiv.org/abs/2601.13996 [4] A. Miranskyy, L. Zhang, and J. Doliskani, “Is your quantum program bug-free?” arXiv preprint arXiv:2001.10870, 2020. [5] D. Kim, H. Khoramrokh, L. Zhang, and A. Miranskyy, “Detecting flaky tests in quantum software: A dynamic approach,” arXiv preprint arXiv:2512.18088, 2025. [6] L. Zhang, M. Radnejad, and A. Miranskyy, “Identifying flakiness in quantum programs,” in 2023 ACM/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM). IEEE, 2023, pp. 1–7. [7] A. Virani, Devraj, A. Suresh, L. Zhang, and M. P. Rao, “Distinguishing quantum software bugs from hardware noise: A statistical approach,” in 2025 IEEE International Conference on Quantum Computing and Engineering (QCE), vol. 1. IEEE, 2025, pp. 837–848. [8] D. D. Awschalom, H. Bernien, R. Hanson, W. D. Oliver, and J. Vučković, “Challenges and opportunities for quantum information hardware,” Science, vol. 390, no. 6777, pp. 1004–1010, 2025. [9] S. Dutta, O. Legunsen, Z. Huang, and S. Misailovic, “Testing probabilistic programming systems,” in Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018, pp. 574–586. [10] J. M. Bernardo and R. Rueda, “Bayesian hypothesis testing: A reference approach,” International Statistical Review, vol. 70, no. 3, pp. 351–372, 2002. [11] D. C. McKay, T. Alexander, L. Bello, M. J. Biercuk, L. Bishop, J. Chen, J. M. Chow, A. D. Córcoles, D. Egger, S. Filipp et al., “Qiskit backend specifications for openqasm and openpulse experiments,” arXiv preprint arXiv:1809.03452, 2018. [12] Y.-H. Kim, S. P. Kulik, and Y. Shih, “Quantum teleportation of a polarization state with a complete bell state measurement,” Physical Review Letters, vol. 86, no. 7, p. 1370, 2001. [13] M. A. Nielsen and I. L. Chuang, Quantum computation and quantum information. Cambridge university press, 2010. [14] J. Choi and J. Kim, “A tutorial on quantum approximate optimization algorithm (qaoa): Fundamentals and applications,” in 2019 international conference on information and communication technology convergence (ICTC). IEEE, 2019, pp. 138–142. [15] M. X. Goemans and D. P. Williamson, “Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming,” Journal of the ACM (JACM), vol. 42, no. 6, pp. 1115– 1145, 1995. [16] L. Zhou, S.-T. Wang, S. Choi, H. Pichler, and M. D. Lukin, “Quantum approximate optimization algorithm: Performance, mechanism, and implementation on near-term devices,” Physical Review X, vol. 10, no. 2, p. 021067, 2020. [17] IBM, “IBM Quantum Platform Compute Resources,” Jan. 2026. [Online]. Available: https://quantum.cloud.ibm.com/computers [18] P. Zuliani, A. Platzer, and E. M. Clarke, “Bayesian statistical model checking with application to stateflow/simulink verification,” Formal Methods in System Design, vol. 43, no. 2, pp. 338–367, 2013. [19] H. Erdogmus, “Bayesian hypothesis testing illustrated: An introduction for software engineering researchers,” ACM Computing Surveys, vol. 55, no. 6, pp. 1–28, 2022. [20] A. Miranskyy, “The cost of certainty: Shot budgets in quantum program testing,” arXiv preprint arXiv:2510.22418, 2025. [21] J. B. Spring, B. J. Metcalf, P. C. Humphreys, W. S. Kolthammer, X.-M. Jin, M. Barbieri, A. Datta, N. Thomas-Peter, N. K. Langford, D. Kundys et al., “Boson sampling on a photonic chip,” Science, vol. 339, no. 6121, pp. 798–801, 2013. [22] A. Bouland, B. Fefferman, C. Nirkhe, and U. Vazirani, “On the complexity and verification of quantum random circuit sampling,” Nature Physics, vol. 15, no. 2, pp. 159–163, 2019.
[23] J. Martı́nez-Cifuentes, K. M. Fonseca-Romero, and N. Quesada, “Classical models may be a better explanation of the jiuzhang 1.0 gaussian boson sampler than its targeted squeezed light model,” Quantum, vol. 7, p. 1076, 2023. [24] J. Martı́nez-Cifuentes, H. de Guise, and N. Quesada, “Linear crossentropy certification of quantum computational advantage in gaussian boson sampling,” PRX Quantum, vol. 5, no. 4, p. 040312, 2024. [25] M. Wang, B. Fang, A. Li, and P. J. Nair, “Red-qaoa: Efficient variational optimization through circuit reduction,” in Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, 2024, pp. 980–998.