Pith. sign in

REVIEW 5 minor 36 references

Automated Expected Cost Analysis for Quantum Programs

T0 review · 0 major / 5 minor · reviewed 2026-07-13 · grok-4.5

Challenge this review Download PDF Read on arXiv ↗

Pith's one-line read A fully automatic tool can now bound the expected cost of mixed classical-quantum programs that use mid-circuit measurements and loops.

desk verdict Solid first automation of quantum expected-cost analysis for dynamic programs; the tool works and recovers known tight bounds. read the letter →

arxiv 2604.03971 v1 submitted 2026-04-05 cs.PL

Georg Moser , Michael Schaper This is my paper
classification cs.PL
keywords quantumprogramsexpectedcostanalysisstaticexpectationtransformermid-circuitmeasurementclassicalcontrolflowrepeat-until-success
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

Writing quantum programs that mix classical control with mid-circuit measurements remains error-prone and hard to reason about by hand. This paper presents Qet, a static analyser that takes an imperative mixed classical-quantum program and returns a sound upper bound on its expected cost (or reports that it cannot find one). The method rests on a term-based reformulation of the quantum expectation transformer: symbolic density-matrix fragments are propagated through the program, loop bodies produce upper-invariant constraints, those constraints are reduced to polynomial inequalities, and an SMT solver synthesises a certificate. On a suite of literature examples—including repeat-until-success circuits and weak-measurement variants of Grover search—the tool recovers the tightest previously known bounds automatically. The result matters because existing resource estimators handle only static circuits; Qet is the first tool that can reason about the expected runtime of the dynamic algorithms that real devices already execute.

What carries the argument

The quantum expectation transformer, realised as a symbolic term-based inference system that turns loop upper-invariance into cost-expression templates and finally into polynomial certificate constraints solved by SMT.

What would settle it

Take any of the benchmark programs whose literature bound is already known (e.g. the RUS circuit with success probability 5/8) and check whether Qet returns a strictly weaker certificate or fails to return a bound at all under the same template heuristics.

Watch

Extended reading notes

Core claim

Qet can fully automatically derive precise upper bounds on the expected cost of mixed classical-quantum programs that contain mid-circuit measurements and classical control flow; the bounds match the tightest results previously obtained only by tedious hand calculation.

Load-bearing premise

The analysis succeeds only when a hand-chosen family of cost templates and a heuristically selected subset of density-matrix entries are rich enough for the SMT solver to find a model; otherwise it simply returns “Unknown”.

Editorial extensions

If this is right

  • Dynamic algorithms that rely on mid-circuit measurement (repeat-until-success, weak Grover search, measurement-based walks) can now be given fully automatic expected-cost certificates instead of manual calculations.
  • Existing hardware-specific resource estimators that handle only static circuits can be complemented by a front-end that accounts for classical control and probabilistic termination.
  • Loop-heavy quantum programs become amenable to modular bottom-up analysis once upper invariants can be synthesised rather than supplied by the user.
  • Soundness of the returned bound is guaranteed by the transformer semantics even when the tool aborts with “Unknown”.
  • The same pipeline can be reused for other quantitative properties expressible as expectations (e.g. expected gate counts of a particular type).

Reading between the lines

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

  • The same symbolic-density-matrix and template machinery could be specialised to restricted gate sets or pure-state fragments to push the qubit limit beyond the current six-qubit examples.
  • Because the transformer already separates cost from value, the tool could be extended to expected-error or fidelity analysis with only local changes to the cost annotations.
  • Failure modes that return “Unknown” supply a concrete signal for when a programmer should switch to a coarser abstract domain or supply an invariant by hand.
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

0 major / 5 minor

Summary. The paper presents Qet, a prototype static analysis tool that automatically derives sound upper bounds on the expected cost of mixed classical-quantum programs written in the IMQ language. The approach rests on a term-based, symbolic reformulation of the quantum expectation transformer of Avanzini et al., which generalises Dijkstra-style predicate transformers to density-operator semantics and mid-circuit measurements. Fixed-point reasoning for loops is replaced by upper-invariant term constraints that are successively reduced to cost expressions, polynomial inequalities and finally certificate constraints solved by an SMT solver (Handelman certificates). Soundness of the symbolic transformer is stated as Theorem 1 and proved by induction in Appendix A.7. Evaluation on a suite of literature examples (repeat-until-success circuits, -X, CHAIN, coin-tossing, specialised quantum walk) recovers the previously known tight bounds fully automatically; the largest successful instance uses six qubits and twenty-two measurements.

Significance. If the claims hold, the work supplies the first fully automatic expected-cost analysis for dynamic quantum programs that combine mid-circuit measurements with classical control flow. Existing resource estimators (Azure Quantum Resource Estimator, Qualtran) are restricted to static circuits; verification tools such as SymQV, Silver and AutoQ 2.0 target functional correctness rather than quantitative cost. The paper therefore fills a genuine gap. Strengths that raise confidence include an explicit soundness theorem with a complete inductive proof, a modular constraint pipeline that inherits the upper-invariance law of the underlying semantic framework, and experimental recovery of all previously published manual bounds on the chosen benchmarks. The free parameters of the method (template coefficients and Handelman degree) are existentially quantified unknowns solved by SMT rather than fitted to data, so the analysis is not circular.

minor comments (5)
  1. Section 5.1 and the surrounding text repeatedly use the phrase “density matrix variables” without a single, self-contained definition of the set V of tracked variables; a short formal paragraph would improve readability.
  2. Table 1 reports “?” for QUANTUM-WALK and WMGROVER(k). A one-sentence explanation of the precise unsupported feature (parametrised state space / unsupported unitaries) would make the evaluation self-contained.
  3. The concrete syntax of IMQ is relegated to Appendix A.1; a short illustrative fragment in the main text (beyond the -X example) would help readers unfamiliar with the language.
  4. A few typographical inconsistencies appear (e.g., “RU S” versus “RUS”, “W HILE-X” versus “WHILE-X”). Uniform capitalisation would improve polish.
  5. The Handelman degree n used by the SMT backend is never stated for the successful runs; reporting the maximal degree that was required would aid reproducibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: automation of a prior semantic framework with independent soundness proof and SMT-synthesized certificates

full rationale

The paper's derivation chain starts from the quantum expectation transformer (qet) of Avanzini et al. [4,3] (overlapping author Moser), recalls its universal laws (monotonicity, upper invariance, separation), then introduces a novel syntactic term transformer qinf together with a constraint-reduction pipeline (term constraints o cost constraints o polynomial constraints o certificate constraints solved by Z3). Theorem 1 (Appendix A.7) proves by induction on program structure that any solution of the generated side-conditions yields a sound upper bound relative to qet; free coefficients in the heuristic templates are existentially quantified unknowns, not fitted to data. Evaluation recovers known tight bounds from the literature (including the authors' own prior manual calculations) as an independent check, not as an input that forces the output. Failure of the SMT solver simply returns Unknown while preserving soundness. No equation reduces by construction to an assumed quantity, no uniqueness theorem is imported to forbid alternatives, and no ansatz is smuggled via citation. The self-citation of the foundational transformer is ordinary scientific building-on-prior-work and is not load-bearing for the automation claim itself.

Assumptions & free parameters 1 free parameters · 4 assumptions · 1 invented entities

The paper rests on the already-published quantum expectation transformer semantics, standard density-operator quantum mechanics, and classical techniques for synthesising polynomial ranking functions. No new physical entities or free numerical constants fitted to data are introduced; the only ‘free’ quantities are the existentially quantified template coefficients that the SMT solver is asked to instantiate.

free parameters (1)
  • template coefficients (c_i) and Handelman degree n
    Unknown non-negative reals appearing in cost-expression templates and in the non-negativity certificate; they are solved for by Z3 rather than fitted to external measurements.
assumptions (4)
  • domain assumption Quantum expectation transformer qet[·]{·} correctly characterises expected cost and expected value (Proposition 1, taken from Avanzini et al.)
    The entire automation is proved sound relative to this semantic model; the paper does not re-derive it.
  • domain assumption Density operators are Hermitian positive-semidefinite matrices of trace 1; measurement probabilities are given by the Born rule
    Used throughout the symbolic representation of quantum states (Section 4.1 and 5.1).
  • standard math Handelman’s theorem supplies a complete characterisation of polynomials non-negative on a compact polyhedron (used incompletely with finite degree)
    Invoked in Section 5.5 to turn polynomial inequalities into QF_NRA constraints.
  • domain assumption Clifford+T (plus a few derived gates) is a universal gate set sufficient for the programs under consideration
    Explicit design choice that keeps arithmetic expressions inside Z[√2] (Section 5.1).
invented entities (1)
  • symbolic expectation transformer qinf and the Term language (Fun, Meas, Tick, …)
    purpose: Provide a first-order, constraint-generating representation of the semantic transformer that can be manipulated by an SMT-based synthesis loop
    Defined in Section 5.2; purely a technical device for automation, not a new physical or semantic object.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Automated Expected Cost Analysis for Quantum Programs." pith.science (2026). https://pith.science/paper/2604.03971

@misc{pith2026260403971,
  author       = {Pith},
  title        = {Pith review of: Automated Expected Cost Analysis for Quantum Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2604.03971}},
  note         = {Machine review of arXiv:2604.03971}
}
read the original abstract

In recent years, quantum computing has gained a substantial amount of momentum, and the capabilities of quantum devices are continually expanding and improving. Nevertheless, writing a quantum program from scratch remains tedious and error-prone work, showcasing the clear demand for automated tool support. We present Qet, a fully automated static program analysis tool that yields a precise expected cost analysis of mixed classical-quantum programs. Qet supports programs with advanced features like mid-circuit measurements and classical control flow. The methodology of our prototype implementation is based on a recently proposed quantum expectation transformer framework, generalising Dijkstra's predicate transformer and Hoare logic. The prototype implementation Qet is evaluated on a number of case studies taken from the literature and online references. Qet is able to fully automatically infer precise upper bounds on the expected costs that previously could only be derived by tedious manual calculations.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

36 extracted references · 7 canonical work pages

  1. [1]

    In: Proc

    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Proc. of 15th SAS. LNCS, vol. 5079, pp. 221–237 (2008).https://doi.org/10.1007/978-3-540-69166-2_15

    work page doi:10.1007/978-3-540-69166-2_15 2008

  2. [2]

    Quantum Science and Technology7(2), 025007 (2022).https://doi

    Andrés-Martínez, P., Heunen, C.: Weakly measured while loops: peeking at quan- tum states. Quantum Science and Technology7(2), 025007 (2022).https://doi. org/10.1088/2058-9565/ac47f1

    doi:10.1088/2058-9565/ac47f1 2022

  3. [3]

    In: Proc

    Avanzini, M., Moser, G., Péchoux, R., Perdrix, S.: On the hardness of analyzing quantum programs quantitatively. In: Proc. of 33rd ESOP. LNCS, vol. 14577, pp. 31–58. Springer (2024).https://doi.org/10.1007/978-3-031-57267-8_2

    doi:10.1007/978-3-031-57267-8_2 2024

  4. [4]

    In: Proc

    Avanzini, M., Moser, G., Péchoux, R., Perdrix, S., Zamdzhiev, V.: Quantum ex- pectation transformers for cost analysis. In: Proc. of 37th LICS. pp. 10:1–10:13. ACM (2022).https://doi.org/10.1145/3531130.3533332

    doi:10.1145/3531130.3533332 2022

  5. [5]

    Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. of the ACM on Programming Languages4(OOPSLA), 172:1– 172:30 (2020).https://doi.org/10.1145/3428240

    doi:10.1145/3428240 2020

  6. [6]

    Proceedings of the ACM on Programming Languages7(PLDI), 1050–1072 (2023).https://doi.org/10.1145/3591263

    Avanzini, M., Moser, G., Schaper, M.: Automated expected value analysis of re- cursive programs. Proceedings of the ACM on Programming Languages7(PLDI), 1050–1072 (2023).https://doi.org/10.1145/3591263

    doi:10.1145/3591263 2023

  7. [7]

    Physics Today74(2021).https://doi.org/10.1063/PT.3.4698,https://doi.org/10

    Ball, H., Biercuk, M., Hush, M.: Quantum firmware and the QC Stack. Physics Today74(2021).https://doi.org/10.1063/PT.3.4698,https://doi.org/10. 1063/PT.3.4698

    work page doi:10.1063/pt.3.4698 2021

  8. [8]

    In: Proc

    Bandic, M., Feld, S., Almudéver, C.G.: Full-stack quantum computing systems in the NISQ era: algorithm-driven and hardware-aware compilation techniques. In: Proc. DATA 2022. pp. 1–6 (2022).https://doi.org/10.23919/DATE54114.2022. 9774643

    doi:10.23919/date54114.2022 2022

Show all 36 references
  1. [9]

    In: Proc

    Bauer-Marquart, F., Leue, S., Schilling, C.: SymQV: Automated Symbolic Verifi- cation of Quantum Programs. In: Proc. of 25th FM. LNCS, vol. 14000, pp. 181–198 (2023).https://doi.org/10.1007/978-3-031-27481-7_12

    2023 doi

  2. [10]

    In: Proc

    Bichsel, B., Baader, M., Gehr, T., Vechev, M.: Silq: a high-level quantum lan- guage with safe uncomputation and intuitive semantics. In: Proc. of 41st PLDI. p. 286–300. ACM, New York, USA (2020).https://doi.org/10.1145/3385412. 3386007

    2020 doi

  3. [11]

    ACM38(2016).https://doi.org/10

    Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM38(2016).https://doi.org/10. 1145/2866575

    2016

  4. [12]

    In: Proc

    Chen, Y., Chung, K., Hsieh, M., Huang, W., Lengál, O., Lin, J., Tsai, W.: Autoq 2.0: From verification of quantum circuits to verification of quantum programs. In: Proc. of 31st TACAS. LNCS (2025).https://doi.org/10.1007/ 978-3-031-90660-2_5

    2025

  5. [13]

    In: Proc

    Chen, Y., Chung, K., Lengál, O., Lin, J., Tsai, W.: AutoQ: An Automata-Based Quantum Circuit Verifier. In: Proc. of 35th CAV. LNCS (2023).https://doi.org/ 10.1007/978-3-031-37709-9_7

    2023 doi

  6. [14]

    New Journal of Physics13(4), 043016 (2011)

    Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics13(4), 043016 (2011)

    2011

  7. [16]

    JACM34(4), 325–363 (2005).https: //doi.org/10.1007/S10817-005-9022-X

    Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving ter- mination using polynomial interpretations. JACM34(4), 325–363 (2005).https: //doi.org/10.1007/S10817-005-9022-X

    2005 doi

  8. [17]

    In: Proc

    van Dam, W., Mykhailova, M., Soeken, M.: Using Azure Quantum Resource Es- timator for Assessing Performance of Fault Tolerant Quantum Computation. In: Proc. of SC23. Association for Computing Machinery (2023).https://doi.org/ 10.1145/3624062.3624211

    2023 doi

  9. [18]

    MSCS16(3), 429– 451 (2006).https://doi.org/10.1017/S0960129506005251

    D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. MSCS16(3), 429– 451 (2006).https://doi.org/10.1017/S0960129506005251

    2006 doi

  10. [19]

    ACM18(8), 453–457 (1975).https://doi.org/10.1145/360933.360975

    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of pro- grams. ACM18(8), 453–457 (1975).https://doi.org/10.1145/360933.360975

    1975 doi

  11. [20]

    In: Proc

    Feng, Y., Hahn, E.M., Turrini, A., Zhang, L.: QPMC: A model checker for quantum programs and protocols. In: Proc. of 20th FM. LNCS (2015).https://doi.org/ 10.1007/978-3-319-19249-9_17

    2015 doi

  12. [21]

    Greengard, S.: A quantum leap forward. Comm. ACM68(8), 17–19 (2025).https: //doi.org/10.1145/3735503

    2025 doi

  13. [22]

    Performance Evaluation 73, 110–132 (2014).https://doi.org/10.1016/j.peva.2013.11.004

    Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation se- mantics for the probabilistic guarded command language. Performance Evaluation 73, 110–132 (2014).https://doi.org/10.1016/j.peva.2013.11.004

    2014 doi

  14. [23]

    PJM132(1), 35–62 (1988).https://doi.org/http: //dx.doi.org/10.2140/pjm.1988.132.35

    Handelman, D.: Representing Polynomials by Positive Linear Functions on Com- pact Convex Polyhedra. PJM132(1), 35–62 (1988).https://doi.org/http: //dx.doi.org/10.2140/pjm.1988.132.35

    1988 doi

  15. [24]

    Harrigan, M.P., Khattar, T., Yuan, C., Peduri, A., Yosri, N., Malone, F.D., Bab- bush, R., Rubin, N.C.: Expressing and analyzing quantum algorithms with qual- tran (2024).https://doi.org/10.48550/arXiv.2409.04643

    2024 doi arXiv

  16. [25]

    ACM12(10), 576–580 (1969).https://doi.org/10.1145/363235.363259

    Hoare, C.A.R.: An axiomatic basis for computer programming. ACM12(10), 576–580 (1969).https://doi.org/10.1145/363235.363259

    1969 doi

  17. [26]

    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest Precondition Rea- soningforExpectedRuntimesofRandomizedAlgorithms.JACM65(5),30:1–30:68 (2018).https://doi.org/https://doi.org/10.1145/3208102

    2018 doi

  18. [27]

    In: Foundations of Probabilistic Programming.https://doi.org/10

    Kaminski, B.L., Katoen, J., Matheja, C.: Expected runtime analysis by program verification. In: Foundations of Probabilistic Programming.https://doi.org/10. 1017/9781108770750.007

  19. [28]

    LANL Report LAUR-96-2724 (1996),https://arxiv.org/abs/2211.02559

    Knill, E.: Conventions for quantum pseudocode. LANL Report LAUR-96-2724 (1996),https://arxiv.org/abs/2211.02559

    1996 arXiv

  20. [29]

    In: Proc

    Lewis, M., Zuliani, P., Soudjani, S.: Automated verification of silq quantum pro- grams using SMT solvers. In: Proc. of 3rd QSW. pp. 125–134 (2024).https: //doi.org/10.1109/QSW62656.2024.00027

    2024 doi

  21. [30]

    JACM (2025).https://doi.org/ 10.1145/3734516

    Liu, J., Zhou, L., Ying, G.B.M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. JACM (2025).https://doi.org/ 10.1145/3734516

    2025 doi

  22. [31]

    ACM SIGPLAN Notices53(4), 496–512 (2018)

    Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource anal- ysis for probabilistic programs. ACM SIGPLAN Notices53(4), 496–512 (2018). https://doi.org/10.1145/3296979.3192394

    2018 doi

  23. [32]

    Cam- bridge University Press, 2nd edn

    Nielsen, M., Chuang, I.: Quantum Computation and Quantum Information. Cam- bridge University Press, 2nd edn. (2010)

    2010

  24. [33]

    Quantum Information & Computation14(15-16), 1277– 1301 (2014).https://doi.org/10.26421/QIC14.15-16-2

    Paetznick, A., Svore, K.M.: Repeat-until-success: non-deterministic decomposition of single-qubit unitaries. Quantum Information & Computation14(15-16), 1277– 1301 (2014).https://doi.org/10.26421/QIC14.15-16-2

    2014 doi

  25. [34]

    Paltenghi, M., Pradel, M.: Bugs in quantum computing platforms: an empirical study6(OOPSLA1), 1–27 (2022).https://doi.org/10.1145/3527330 Automated Expected Cost Analysis for Quantum Programs 21

    2022 doi

  26. [35]

    Physical review A68(2), 022312 (2003)

    Raussendorf, R., Browne, D.E., Briegel, H.J.: Measurement-based quantum com- putation on cluster states. Physical review A68(2), 022312 (2003)

    2003

  27. [36]

    Mathematical Struc- tures in Computer Science14(4), 527–586 (2004).https://doi.org/10.1017/ S0960129504004256

    Selinger, P.: Towards a quantum programming language. Mathematical Struc- tures in Computer Science14(4), 527–586 (2004).https://doi.org/10.1017/ S0960129504004256

    2004

  28. [37]

    In: Proc

    Wang,P.,Fu,H.,Goharshady,A.K.,Chatterjee,K.,Qin,X.,Shi,W.:CostAnalysis of Nondeterministic Probabilistic Programs. In: Proc. of PLDI 2019. pp. 204–220. PLDI 2019, ACM (2019).https://doi.org/10.1145/3314221.3314581 22 G. Moser and M. Schaper A Appendix A.1 Syntax The syntax gra...

    2019 doi

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.