Pith. sign in

REVIEW 2 major objections 4 minor 33 references

Noise-aware Verification and Synthesis of Quantum Programs

T0 review · 2 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A new quantum Hoare logic verifies and synthesizes programs against real hardware noise, using ensembles rather than density matrices as the semantic primitive.

desk verdict The verification semantics is a genuine contribution; the synthesis optimality theorem is false as stated, so this needs a major revision before the hardware-optimal claims can be trusted. read the letter →

arxiv 2608.05807 v1 pith:GKYW4QGL submitted 2026-08-06 cs.PL cs.FLcs.LO

Stefanie Muroya , Krishnendu Chatterjee , Thomas A. Henzinger This is my paper · ORCID
classification cs.PLcs.FLcs.LO
keywords quantumHoarelogicnoisyhardwareerrormodelsensemblesemanticsdensitymatricesprogramsynthesisverificationprobabilisticbranching
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper attempts to make quantum program correctness depend on the actual hardware a program will run on. It develops a quantum Hoare logic, nQHL, whose assertions are interpreted over ensembles—probability distributions over classical-quantum states—rather than density matrices, and whose proof rules are parameterised by vendor-published error models for gates and measurements. On top of this logic the paper builds a decision procedure for verifying loop-free programs with linear preconditions, and a synthesis method that, given any linear precondition and target postcondition, returns a program of bounded length that is optimal among all admissible programs for reaching the target set. This matters because short subroutines such as parity checks, state reset, and state discrimination behave differently on different noisy devices, and the synthesized programs beat the textbook noise-free solutions on the vendor hardware specifications used in the evaluation. The paper also reports that classical probabilistic branching can be strictly necessary for optimality, not merely a convenience.

What carries the argument

The load-bearing object is the ensemble: a finite probability distribution over hybrid states, each hybrid state being a pure quantum state together with an assignment of the classical bits. A hardware specification assigns to every unitary instruction a completely positive trace-preserving set of noise operators and to every measurement a four-entry error matrix, which turns each instruction into a probabilistic successor function on ensembles; these successor functions give the semantics of the programming language and the transitions of the ensemble graph. The ensemble graph is the verification engine: an infinite Markov chain whose states are configurations (program plus ensemble), and for loop-free programs only a finite part reachable within the horizon is explored, with linear preconditions handled by checking the corners of each polytope via convexity. Synthesis is carried by two constructions: the recursive DCP/CondBlock enumeration, which builds the finite set of dominant deterministic programs of length at most $k$, and the maximin linear program of Equation 12, which assigns each dominant program a probability so that the worst-case reachability probability over all initial ensembles is maximized; for a unique initial ensemble, Bellman value iteration on a quantum-belief game graph plays the same role. The Hoare rules HM00–HM01 and HUnitary carry the logic itself, expressing each noisy step as a convex combination of branches weighted by noise probabilities.

What would settle it

Enumerate every loop-free program of length at most $k$ over a small instruction set (two classical bits, one measurement, a few gates) on a fixed vendor hardware specification, and compare the best worst-case reachability found by brute force against the value returned by the paper's linear-programming synthesis; if any brute-forced program beats the LP solution, the enumeration underlying Lemma 5.1 is incomplete and the hardware-optimality guarantee holds only within the enumerated set.

Watch

Extended reading notes

Core claim

nQHL is the first quantum Hoare logic whose assertions are interpreted over arbitrary ensembles and the first to incorporate hardware error models, and the paper argues that both features are needed for modular reasoning about subroutines on real devices. The central conceptual claim is that ensembles, not density matrices, are the right semantic primitive: two different ensembles can have the same density matrix yet evolve under the same gate into globally distinguishable states, so a subroutine that correctly prepares a local Bell state from one ensemble realization can fail from another, and no density-matrix logic can express the difference. The proof system is shown sound, with noisy measurement and unitary instructions handled by rules that decompose each instruction into branches weighted by the probabilities of the hardware's noise operators. On the algorithmic side, verification of loop-free programs under linear preconditions is reduced to model checking a finite part of an ensemble graph, checking only the corners of each polytope of initial ensembles; and bounded synthesis for target postconditions is reduced to a maximin linear program that mixes finitely many deterministic candidate programs. The paper claims the resulting program is hardware-optimal—that is, it reaches the target set with the highest worst-case probability among all admissible loop-free programs of length at most $k$—and that when the precondition covers two or more ensembles, the optimal program can genuinely require classical probabilistic branching, as in the state-discrimination task where a 50/50 mixture attains 0.75 worst-case success while every deterministic program attains only 0.5.

Load-bearing premise

The synthesis method's guarantee of hardware-optimality rests on the assumption that its candidate list contains every admissible program of the chosen length; this is justified by an invoked game-theory theorem rather than a full proof, so if the list omits a program, optimality holds only within the list.

Editorial extensions

If this is right

  • The same logical subroutine can be provably optimal for one device and suboptimal for another: the synthesized programs differ across hardware specifications and embeddings, and they differ from textbook noise-free solutions.
  • Modular verification becomes possible without knowing the global state: a subroutine proven correct under ensemble semantics keeps its guarantee for every ensemble realization consistent with a given reduced density matrix, which no density-matrix logic can express.
  • Optimal quantum programming may require classical probabilistic branching: for the state-discrimination task even the noise-free optimum is a 50/50 mixture achieving 0.75 worst-case success versus 0.5 for any deterministic program.
  • Bounded verification and synthesis run with exact rational arithmetic, giving quantitative reachability guarantees to a stated precision rather than only yes/no correctness, with the required precision growing polynomially in the program depth.
  • For common subroutines such as error-correction parity checks, state reset, and GHZ and Bell-state preparation, hardware-aware synthesis improves on textbook majority-vote programs by up to tens of percentage points on the tested vendor specifications.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural extension would run the verification procedure on pairs of global states with identical partial trace but different local ensemble structure (as in the Bell-state example); any tool built on density-matrix semantics must miss such cases by construction, so such pairs form a ready-made benchmark for separating the two semantics.
  • If the enumeration lemma is later proved complete, the same linear-programming core should scale to instruction sets with more classical state, where the space of behavioral strategies is much larger and mixed strategies are likely to matter even more.
  • The paper establishes only bounded-horizon guarantees and notes that unbounded reachability is undecidable even without noise; a natural follow-up is to study how per-horizon optimal values behave as the horizon grows on fixed hardware, whether they converge in practice, and how close bounded programs come to that limit.
  • The necessity of probabilistic branching for optimality suggests that noisy-hardware compilers should treat classical random choice as essentially free: mixing two or three deterministic strategies could buy substantial accuracy without adding a single quantum gate.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper develops a comprehensive framework for reasoning about quantum programs executed on noisy hardware. It introduces nQHL, a Hoare logic interpreted over ensembles (probability distributions over classical-quantum states) rather than density matrices, with proof rules parameterized by hardware error models; soundness is proved in the appendix (Theorem 3.1). It then presents an automated verification procedure (checkLin) for loop-free programs with linear preconditions, based on exploring ensemble graphs and encoding postcondition satisfaction in the first-order theory of real-closed fields; correctness is proved in the appendix (Theorem 4.3). For synthesis, the paper reduces bounded synthesis to enumeration of a finite set A_k of deterministic programs (Eq. (8), DCP/CondBlock), then computes optimal probabilistic mixtures by linear programming for target postconditions (Theorem 5.2) and by Bellman value iteration on quantum-belief game graphs for singular preconditions (Theorem 5.3). Experiments on five quantum subroutines across 55 IBM Qiskit hardware specifications report hardware-dependent optimal programs, frequently using probabilistic branching. The synthesis claims for linear preconditions rest on Lemma 5.1, which the main text justifies only by a one-paragraph appeal to Kuhn's theorem. Section 3.3 explicitly states that relative completeness of the logic is not studied, a reasonable scope limitation.

Significance. If the results held as stated, this would be a strong and timely contribution. The ensemble semantics is well motivated (Examples 1 and 2 show that density-matrix abstractions lose information needed for modular subroutine verification), the soundness proof of nQHL and the correctness proof of checkLin in the appendix appear correct, the arbitrary-precision treatment of verification is rigorous, and the evaluation across 55 hardware specifications is substantial. The paper also builds on and generalizes the authors' prior work [19] rather than duplicating it. However, the 'hardware-optimal' synthesis guarantee for linear preconditions is false as stated: Lemma 5.1 is contradicted by a concrete counterexample, and the optimality clause of Theorem 5.2 therefore fails (see Major Comments). The verification and logic contributions remain valuable; the synthesis contribution needs either a strengthened enumeration with a genuine completeness proof or a re-scoping of its claims.

major comments (2)
  1. [Section 5.1, Lemma 5.1 and Eq. (8)] Lemma 5.1 is false as stated. Consider ideal hardware, one qubit q0, one classical bit x, instruction set J={H([q0]), X([q0])}, horizon k=1, linear precondition φ := {P([q0]=|0> ∧ [x]=0)=1} ∨ {P([q0]=|1> ∧ [x]=1)=1} (two singleton polytopes), and target postcondition ψ := P([q0]=|+> ∨ [q0]=|0>)=1. The program P := if(x){X([q0])}else{H([q0])} is a candidate program of length 1, is admissible under the trivial guard, and {φ}P{ψ} is valid: from β0=(|0>,x=0) it takes the else-branch and reaches |+>, and from β1=(|1>,x=1) it takes the then-branch and reaches |0>. However, DCP(β0,1)=DCP(β1,1)={halt, H;halt, X;halt}: since |CStates(JJK_H(β))|=1 for every instruction applied to a corner, the CondBlock clause of Eq. (8) is never triggered, and A_1 contains no program whose first action is a conditional. For any convex combination of A_1 programs, the success probability from β0 is p_halt+p_H while from β1 it is p_X; validity of the triple requires both to equal 1, which is impossible (p_X=0 and p_X=1 simultaneously). The LP in Eq. (12) over A_1 therefore returns max p=0.5, whereas P achieves p=1. The root cause is that DCP is applied corner-by-corner and never branches on a classical variable that is non-constant across the precondition. The one-paragraph invocation of Kuhn's theorem does not repair this: the omitted programs are pure strategies, not mixed strategies, so the theorem is inapposite to the completeness of the enumeration.
  2. [Section 5.2, Theorem 5.2 and Eq. (12)] Theorem 5.2 inherits the failure of Lemma 5.1. Its optimality claim ('Moreover, Σ x_i P_i is optimal for the precondition φ and target φ') quantifies over all admissible programs of length at most k, but Eq. (12) only optimizes over the rows M_{ij} given by the incomplete set A_k (or A^{φ,φ}_k). The counterexample of Major Comment 1 shows the LP optimum (0.5) is strictly below the value achievable by an admissible length-1 program (1). The appendix (Section 10.1) does not prove Lemma 5.1; its proof of Theorem 5.2 simply states that 'we consider all deterministic programs that satisfy the instruction guard and are of length at most k,' which is precisely the completeness claim refuted above. Consequently, the 'hardware-optimal' wording in the abstract, the introduction, and in the linear-precondition experiments of Section 6.2 is unsupported for linear preconditions. The statement can be repaired either by extending the DCP/CondBlock enumeration to branch on the classical state of the initial ensemble (equivalently, partitioning the precondition's ensembles into beliefs before any instruction, as Section 5.3 already does for singular preconditions) and proving completeness of the extended enumeration over all length-≤k programs, or by explicitly restricting all optimality claims to the enumerated program family and re-framing the experiments accordingly. Note that in all benchmarks of Section 6 the initial classical state is constant (x0=0) across corners, so the reported numbers may survive the repair, but the claimed guarantees need re-statement.
minor comments (4)
  1. [Section 4.2 (definition of linear assertion)] The definition φ_Ω := ⋁_{P∈Ω} (⋀_{β∈P} φ_β), with φ_β singular, is not coherent for polytopes with more than one corner: the conjunction of two distinct singular assertions is unsatisfiable, yet Example 4 treats a two-corner polytope as a satisfiable precondition and Algorithm 1 iterates over conv(P) semantics. Please define polytope assertions directly (e.g., φ_P denotes the set conv(P)) and state the linearity assumption with that semantics.
  2. [Section 5.2 (precision bound after Theorem 5.2)] The bound (N+1)·ρ·(k+1)+((N+1)/2)·log(N+1) for exactly solving Eq. (12) is asserted without proof, and citation [5] (Bland) guarantees finite termination only for the simplex method with a specific pivoting rule, not for arbitrary solvers. Please supply a derivation or restate the bound as a property of the implemented arbitrary-precision simplex procedure.
  3. [Section 7 (Conclusion)] The closing sentence says that game-theoretic synthesis of hardware-optimal programs with 'more general preconditions' is left as an open challenge, which conflicts with Section 5.2's claim of optimality for all linear preconditions; please clarify the scope of both statements in light of the issues with Lemma 5.1.
  4. [Section 3.3 and Section 1.2] The paper explicitly states that relative completeness of nQHL is not studied; given the novelty claims for the logic, I suggest adding a short discussion of what a completeness result for the loop-free fragment would require, so readers can calibrate the logic's power in comparison with dense-matrix-based logics.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the new Hoare logic, verification reduction, and LP-based synthesis are built from explicit semantics and standard mathematical facts; the only self-citation is to a peer-reviewed prior article.

full rationale

The paper's central derivation chain is self-contained rather than circular. The ensemble assertion language is given an independent semantics in Figures 2 and 3, and the Hoare rules are proved sound against the operational semantics in Theorem 3.1 and Appendix 8.1; no assertion is defined in terms of the triple it is used to prove. The verification procedure checkLin reduces linear preconditions to corner ensembles using proved linearity lemmas (Sections 9.1-9.3), and the realForm translation mirrors the assertion semantics exactly (Lemma 4.2). The synthesis method solves a genuine optimization problem: Equation 12 is a maximin linear program whose coefficients are computed from transition probabilities and target-set probabilities, so the resulting probabilities are outputs of an optimization, not fitted parameters renamed as predictions. The only load-bearing citation to the authors' own prior work is [19], used for singular-precondition synthesis (Theorem 5.3) and precision bounds; this is a peer-reviewed published article, and the paper re-runs the same benchmark suite and confirms results by numerical hardware simulation, so it is independent support rather than a circular chain. Lemma 5.1's completeness is asserted via Kuhn's theorem without a detailed proof; if the DCP/CondBlock enumeration omits valid programs, the hardware-optimality claim would be false as a correctness matter, but that is not a circular reduction because the LP's inputs do not include the target postcondition as a constraint that definitionally forces its own output. No equation in the paper is equivalent to its inputs by construction.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

The central claims rest on standard mathematical facts (convexity, real-closed fields, Kuhn's theorem, Bellman optimality) and on domain assumptions about how hardware noise is modeled: CPTP channels for unitary instructions, outcome-flip probabilities for measurements, and the accuracy of vendor-published Qiskit specifications. No free parameter is fitted to data in the derivations; hardware error rates enter as given inputs. No new physical entities are postulated.

assumptions (7)
  • domain assumption Hardware noise is modeled as CPTP channels with finite sets of noise operators per unitary instruction, and measurement noise as outcome-flip probabilities zeta(i,j)
    Section 2.3 defines hardware specifications this way; the semantics and all theorems operate on this model.
  • domain assumption Only single-qubit computational-basis measurements are supported, and noise flips classical outcomes but not the post-measurement state basis
    Section 2.2 and 2.3; the proof rules HM00-HM01 and the experimental MZMX and Reset instruction sets rely on this.
  • standard math Kuhn's theorem equating mixed and behavioral strategies over finite horizons with perfect recall
    Invoked in Section 5.1 to justify Lemma 5.1 for the synthesis reduction.
  • standard math finalEnsemble is linear in the initial ensemble, and reachable sets are convex hulls of images of polytope corners
    Proved as Lemmas 9.1-9.3 in the appendix; underlies checkLin and the LP formulation.
  • standard math The first-order theory of real-closed fields is decidable and exactly solvable with a tool such as Z3
    Used in Section 4.1 (realForm) and Section 5.1 (Equation 10); the paper reports Z3 4.15.4 results.
  • domain assumption Vendor-published Qiskit hardware specifications accurately characterize device error behavior
    Section 6: all experimental claims about hardware-optimality are computed against these specifications, and the 'numerical hardware simulations' confirmation is not detailed.
  • standard math Unbounded reachability for quantum programs is undecidable even in the noise-free case
    Cited from [4] in Section 1.3; motivates the bounded, loop-free, fixed-horizon scope of the algorithms.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Noise-aware Verification and Synthesis of Quantum Programs." pith.science (2026). https://pith.science/paper/GKYW4QGL

@misc{pith2026260805807,
  author       = {Pith},
  title        = {Pith review of: Noise-aware Verification and Synthesis of Quantum Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GKYW4QGL}},
  note         = {Machine review of arXiv:2608.05807}
}
read the original abstract

While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We consider the error models published by quantum hardware vendors to give a hardware-dependent semantics to quantum programs. This work presents a comprehensive study of noise-aware quantum programming, ranging from logical foundations to automated verification and synthesis. We develop a noise-aware quantum Hoare logic, and use it to derive algorithmic methods for the bounded verification of quantum programs on specific hardware, and for the automatic synthesis of noise-optimal loop-free quantum programs. In this way, we synthesize hardware-dependent subroutines that commonly occur in quantum algorithms, such as parity checks, quantum state preparation, and quantum state discrimination. We evaluate our method on the hardware specifications provided by the IBM Qiskit toolkit. Besides finding different optimal subroutines for different noise models, our synthesis tool also shows that classical probabilistic branching is needed for optimality in quantum programming.

Figures

Figures reproduced from arXiv: 2608.05807 by the authors.

Figure 1
Figure 1. The transformer considers the zero subensemble (only) because the if ... else and while statements normalizations may yield the zero subensemble. JskipK𝐻 (𝛽) = 𝛽 J𝑥 := 𝑏K𝐻 (𝛽 ) = Í ℎ∈Supp𝛽 𝛽 (ℎ) · J⟨𝑥, 𝑏⟩K(ℎ), ∀𝑏 ∈ {0, 1} J𝑥0 := 𝑥1K𝐻 (𝛽 ) = Í ℎ∈Supp(𝛽) 𝛽 (ℎ) · J⟨𝑥0, ℎ(𝑥1 ) ⟩K(ℎ) J𝑈 ( −→𝑞 )K𝐻 (𝛽 ) = Í ℎ∈Supp𝛽 𝛽 (ℎ) · J⟨𝑈 , −→𝑞 ⟩K𝐻 (ℎ) J𝑥 := measure(𝑞)K𝐻 (𝛽 ) = Í ℎ∈Supp𝛽 𝛽 (ℎ) · J⟨𝑞, 𝑥 ⟩K𝐻 (ℎ) Jif(𝑥) {𝑃0 } else {𝑃1 }K… view at source ↗
Figure 2
Figure 2. Syntax of terms and assertions. −→𝑞 = [𝑞0, . . . , 𝑞𝑑 ] −→𝑥 = [𝑥0, . . . , 𝑥𝑑 ] ℎ = ( |𝛼⟩ , 𝑐 ) in M𝑄,X 𝛽 ∈ D (M𝑄,X ) signature semantics JQTermK : M𝑄,X → (H≤𝑛 → H≤𝑛 ) J −→𝑞 K(ℎ) = Pt−→𝑞 ( |𝛼⟩ ⟨𝛼 | ) J|𝛼⟩K(ℎ) = |𝛼⟩ ⟨𝛼 | J𝑀 · −→𝑞 K(ℎ) = ( (𝑀 · J −→𝑞 K(ℎ) · 𝑀† )/(Tr(𝑀 · J −→𝑞 K(ℎ) · 𝑀† ) ) if Tr(𝑀 · J −→𝑞 K(ℎ) · 𝑀† ) > 0 0 otherwise J𝑀 ∗ −→𝑞 K(ℎ) = 𝑀 · J −→𝑞 K(ℎ) · 𝑀† JPt𝑞 −→0 (𝑞 −→1 )K(ℎ) = Pt𝑞 −→1 \𝑞 −→0 (J𝑞 −→1K(ℎ)… view at source ↗
Figure 3
Figure 3. Semantics of terms and assertions. a linear operator acting on H−→𝑞 . In contrast, the subscript of quantum term Pt−→𝑞 specifies that −→𝑞 should be removed. The quantum terms 𝑀 · −→𝑞 and 𝑀 ∗ −→𝑞 return the (partial) density operator that results from applying 𝑀 to the reduced density operator over −→𝑞 . The difference is that 𝑀 · −→𝑞 normalizes the result, whereas 𝑀 ∗ −→𝑞 preserves the resulting trace. The classical… view at source ↗
Figures from the paper (23 more)
Figure 4
Figure 4. Figure 4: Hardware-independent proof rules. We write [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 5
Figure 5. Figure 5: Proof rules parameterized by a hardware specification [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Example: Verification of a local Bell-state preparation program. [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 7
Figure 7. Figure 7: Operational rules for executing a hybrid program on a hardware specification [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]
Figure 8
Figure 8. Figure 8: (a) Example of a hardware-optimal program synthesized with horizon 6 for a robust embedding of the [PITH_FULL_IMAGE:figures/full_fig_p023_8.png]
Figure 9
Figure 9. Figure 9: (a) Optimal program synthesized with horizon 4 for [PITH_FULL_IMAGE:figures/full_fig_p025_9.png]
Figure 10
Figure 10. Figure 10: Running times (in seconds) for verifying the programs synthesized in the experiments exposed in [PITH_FULL_IMAGE:figures/full_fig_p035_10.png]
Figure 11
Figure 11. Figure 11: Example of the baseline program used for [PITH_FULL_IMAGE:figures/full_fig_p036_11.png]
Figure 12
Figure 12. Figure 12: Program achieving the highest improvement using instruction set [PITH_FULL_IMAGE:figures/full_fig_p036_12.png]
Figure 13
Figure 13. Figure 13: Program achieving the improvement in robust embeddings using instruction set [PITH_FULL_IMAGE:figures/full_fig_p037_13.png]
Figure 14
Figure 14. Figure 14: Scatter plots for each horizon showing improvements of synthesized programs using instruction [PITH_FULL_IMAGE:figures/full_fig_p038_14.png]
Figure 15
Figure 15. Figure 15: Synthesized program using the CX+H instruction set for the [PITH_FULL_IMAGE:figures/full_fig_p039_15.png]
Figure 16
Figure 16. Figure 16: Scatter plots for each horizon showing improvements of synthesized programs using instruction [PITH_FULL_IMAGE:figures/full_fig_p039_16.png]
Figure 17
Figure 17. Figure 17: Accuracies achieved by all 12 different programs synthesized for the [PITH_FULL_IMAGE:figures/full_fig_p040_17.png]
Figure 18
Figure 18. Figure 18: (a) Baseline program used for the State discrimination problem with horizon 3. (b) Optimal program for horizon 2 for State discrimination on a Torino embedding [PITH_FULL_IMAGE:figures/full_fig_p040_18.png]
Figure 19
Figure 19. Figure 19: Scatter plots for each horizon showing improvements of synthesized programs for the state dis [PITH_FULL_IMAGE:figures/full_fig_p041_19.png]
Figure 20
Figure 20. Figure 20: Example of the baseline program used for the [PITH_FULL_IMAGE:figures/full_fig_p041_20.png]
Figure 21
Figure 21. Figure 21: Program synthesized with horizon 7 for the [PITH_FULL_IMAGE:figures/full_fig_p042_21.png]
Figure 22
Figure 22. Figure 22: Scatter plots for each horizon showing improvements of synthesized programs for the [PITH_FULL_IMAGE:figures/full_fig_p043_22.png]
Figure 23
Figure 23. Figure 23: Scatter plots for each horizon showing improvements of synthesized programs for the [PITH_FULL_IMAGE:figures/full_fig_p044_23.png]
Figure 24
Figure 24. Figure 24: Example of the baseline program with horizon 3 for the [PITH_FULL_IMAGE:figures/full_fig_p045_24.png]
Figure 25
Figure 25. Figure 25: Scatter plots for each horizon showing improvements of synthesized programs for the [PITH_FULL_IMAGE:figures/full_fig_p045_25.png]
Figure 26
Figure 26. Figure 26: Scatter plots for each horizon showing improvements of synthesized programs for [PITH_FULL_IMAGE:figures/full_fig_p046_26.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 21 canonical work pages

  1. [19]

    Henzinger

    Stefanie Muroya, Krishnendu Chatterjee, and Thomas A. Henzinger. 2025. Hardware-optimal quantum algorithms. PNAS122 (2025), e2419273122. doi:10.1073/pnas.2419273122

    work page doi:10.1073/pnas.2419273122 2025

  2. [1]

    Sohaib Alam, Noah F

    M. Sohaib Alam, Noah F. Berthusen, and Peter P. Orth. 2023. Quantum logic gate synthesis as a Markov decision process.npj Quantum Information9 (2023), 108. doi:10.1038/s41534-023-00766-w

    doi:10.1038/s41534-023-00766-w 2023

  3. [2]

    Richard Bellman. 1954. The theory of dynamic programming.Bull. Amer. Math. Soc.60 (1954), 503–515. doi:10.1090/ S0002-9904-1954-09848-8

    work page 1954

  4. [3]

    Charles H. Bennett. 1992. Quantum cryptography using any two nonorthogonal states.PRL68, 21 (1992), 3121

    work page 1992

  5. [4]

    Nathalie Bertrand and Paulin Fournier. 2013. Parameterized verification of many identical probabilistic timed processes. InFSTTCS. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Wadern, Germany, 501–513

    work page 2013

  6. [5]

    Robert G. Bland. 1977. New finite pivoting rules for the simplex method.Mathematics of Operations Research2, 2 (1977), 103–107

    work page 1977

  7. [6]

    Chadha, P

    R. Chadha, P. Mateus, and A. Sernadas. 2006. Reasoning About Imperative Quantum Programs.ENTCS158 (2006), 19–39. doi:10.1016/j.entcs.2006.04.003 MFPS

    work page doi:10.1016/j.entcs.2006.04.003 2006

  8. [7]

    Cirq Developers. 2025. Cirq. doi:10.5281/zenodo.4062499

    doi:10.5281/zenodo.4062499 2025

Show all 33 references
  1. [8]

    Haowei Deng, Runzhou Tao, Yuxiang Peng, and Xiaodi Wu. 2024. A Case for Synthesis of Recursive Quantum Unitary Programs.PACMPL8, POPL (2024), 1759–1788. doi:10.1145/3632901

    2024 doi

  2. [9]

    Yuxin Deng and Yuan Feng. 2022. Formal semantics of a classical-quantum language.Theoretical Computer Science 913 (2022), 73–93. doi:10.1016/j.tcs.2022.02.017

    2022 doi

  3. [10]

    Ellie D’Hondt and Prakash Panangaden. 2006. Quantum weakest preconditions.MSCS16, 3 (2006), 429–451. doi:10. 1017/S0960129506005251

    2006

  4. [11]

    Yuan Feng, Runyao Duan, Zheng-Feng Ji, and Mingsheng Ying. 2007. Proof rules for the correctness of quantum programs.TCS386, 1-2 (2007), 151–166. doi:10.1016/j.tcs.2007.06.011

    2007 doi

  5. [12]

    Florian Fürrutter, Gorka Muñoz-Gil, and Hans J. Briegel. 2024. Quantum circuit synthesis with diffusion models. Nature Machine Intelligence6 (2024), 1–10. doi:10.1038/s42256-024-00831-9

    2024 doi

  6. [13]

    Zi-Hao Guo and Ting-Chi Wang. 2024. SMT-Based Layout Synthesis Approaches for Quantum Circuits. InISPD (ISPD ’24). ACM, New York, NY, USA, 93–100. doi:10.1145/3626184.3633316

    2024

  7. [14]

    Yoshihiko Kakutani. 2009. A Logic for Formal Verification of Quantum Programs. InASIAN, Anupam Datta (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 79–93

    2009

  8. [15]

    Chan Gu Kang and Hakjoo Oh. 2023. Modular Component-Based Quantum Circuit Synthesis.PACMPL7, OOPSLA1, 2493–2520. doi:10.1145/3586039

    2023 doi

  9. [16]

    Harold W. Kuhn. 1953. Extensive games and the problem of information.Contributions to the Theory of Games2, 28 (1953), 193–216

    1953

  10. [17]

    Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. InCA V (Lecture Notes in Computer Science, Vol. 11562), Isil Dillig and Serdar Tasiran (Eds.). ...

    2019 doi

  11. [18]

    Priyanka Mukhopadhyay. 2024. Synthesizing Toffoli-optimal quantum circuits for arbitrary multi-qubit unitaries. arXiv:2401.08950

    2024 arXiv

  12. [20]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2016.Quantum Computation and Quantum Information (10th Anniversary edition). Cambridge University Press, Cambridge, UK

    2016

  13. [21]

    John Preskill. 2018. Quantum computing in the NISQ era and beyond.Quantum2 (2018), 79

    2018

  14. [22]

    Pusey, Jonathan Barrett, and Terry Rudolph

    Matthew F. Pusey, Jonathan Barrett, and Terry Rudolph. 2012. On the reality of the quantum state.Nature Physics8, 6 (2012), 475–478

    2012

  15. [23]

    2023 (accessed February 7, 2025)

    Qiskit contributors. 2023 (accessed February 7, 2025). Qiskit: An Open-Source Framework for Quantum Computing. https://zenodo.org/records/2562111. doi:10.5281/zenodo.2573505

    2023

  16. [24]

    Quantinuum. 2025. Quantinuum Systems. https://www.quantinuum.com/. Accessed: 2025-11-02

    2025

  17. [25]

    Robert Rand. 2019. Verification Logics for Quantum Programs. arXiv:1904.04304 [cs.LO]

    2019 arXiv

  18. [26]

    Xin Sun, Xingchi Su, Xiaoning Bian, and Huiwen Wu. 2024. On the Relative Completeness of Satisfaction-based Quantum Hoare Logic. arXiv:2405.01940

    2024 arXiv

  19. [27]

    Dominique Unruh. 2019. Quantum Hoare Logic with Ghost Variables. InLICS (LICS ’19). IEEE Computer Society, Los Alamitos, CA, USA, 47. doi:10.1109/LICS.2019.8785779

    2019

  20. [28]

    Huiling Wu, Yuxin Deng, and Ming Xu. 2025. Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs. arXiv:2308.04741 [cs.PL]

    2025 arXiv

  21. [29]

    Yao Xiao, Shahin Nazarian, and Paul Bogdan. 2021. A stochastic quantum program synthesis framework based on Bayesian optimization.Scientific Reports11 (2021), 13138. doi:10.1038/s41598-021-91035-3 28 Muroya et al

    2021 doi

  22. [30]

    Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, and Aws Albarghouthi. 2023. Synthesizing Quantum-Circuit Optimizers.PACMPL7 (2023), 835–859. doi:10.1145/3591254

    2023 doi

  23. [31]

    Mingsheng Ying. 2011. Floyd-Hoare logic for quantum programs.TOPLAS33, 6 (2011), 19:1–19:49. doi:10.1145/ 2049706.2049708

    2011

  24. [32]

    Mingsheng Ying. 2024. A Practical Quantum Hoare Logic with Classical Variables, I. arXiv:2412.09869

    2024 arXiv

  25. [33]

    Li Zhou, Nengkun Yu, and Mingsheng Ying. 2019. An Applied Quantum Hoare Logic. InPLDI (PLDI ’19). Association for Computing Machinery, New York, USA, 1149–1162. doi:10.1145/3314221.3314584 Noise-aware Verification and Synthesis of Quantum Programs 29 8 APPENDIX: Proof system 8...

    2019

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.