pith. sign in

arxiv: 2605.14881 · v1 · pith:6FYKEYNQnew · submitted 2026-05-14 · 🪐 quant-ph · cs.LO

QSeqSim: A Symbolic Simulator for Qiskit While Loops Using Sequential Quantum Circuits

Zihao Li , Ji Guan , Mingsheng Ying This is my paper

Pith reviewed 2026-06-30 20:06 UTC · model grok-4.3

classification 🪐 quant-ph cs.LO
keywords quantum simulationwhile loopssequential circuitsbinary decision diagramssymbolic executionQiskitOpenQASM 3
0
0 comments X

The pith

QSeqSim assigns while loops precise sequential circuit semantics and simulates them symbolically via BDDs in Qiskit.

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

The paper introduces QSeqSim as a Qiskit-integrated tool that translates quantum circuits containing while loops into OpenQASM 3 and organizes them into combinational, dynamic, and sequential circuits. It assigns while loops explicit semantics with internal and external qubits, then represents the resulting sequential circuits using structured sparse Binary Decision Diagrams combined with weighted model counting. Dedicated symbolic operators for state composition and retention enable execution across multiple loop iterations without building full state vectors. Experiments show this scales to circuits with over 1000 qubits across more than 10 iterations in a quantum random walk benchmark.

Core claim

QSeqSim takes Qiskit QuantumCircuit objects, translates them into OpenQASM 3 code, organises the resulting program into a combination of combinational, dynamic, and sequential circuits with explicit internal and external qubits for while loops, adopts a BDD-based symbolic representation integrated with weighted model counting to compute measurement probabilities by exploiting sharing, and introduces dedicated symbolic operators for state composition and state retention, thereby enabling efficient symbolic execution of sequential quantum circuits.

What carries the argument

BDD-based symbolic representation with dedicated operators for state composition and retention that exploit sharing in structured and sparse BDDs.

If this is right

  • While-loop quantum programs can be simulated directly inside Qiskit without manual unrolling or external tools.
  • Measurement probabilities for looped circuits become computable by counting models on shared BDD nodes rather than enumerating full state spaces.
  • Sequential quantum circuits induced by loops receive a formal semantics that separates internal loop state from external qubits.
  • Benchmarks with over 1000 qubits and more than 10 iterations become feasible under the sparse BDD assumption.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same BDD operators might apply to other loop-like constructs such as repeat-until-success patterns once their sequential semantics are defined.
  • Integration with existing Qiskit circuit optimizers could reduce BDD size further before symbolic execution begins.
  • The approach suggests a path toward symbolic verification of quantum algorithms whose correctness depends on loop termination conditions.

Load-bearing premise

The structured and sparse BDD representations for while-loop sequential circuits remain computationally tractable without exponential blowup when the dedicated symbolic operators are applied across multiple iterations.

What would settle it

Simulate the quantum random walk benchmark at 2000 qubits for 20 loop iterations and check whether runtime stays polynomial or exhibits exponential growth in memory or time.

Figures

Figures reproduced from arXiv: 2605.14881 by Ji Guan, Mingsheng Ying, Zihao Li.

Figure 1
Figure 1. Figure 1: Classical–quantum analogy from programs to IRs to circuits. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: QSeqSim workflow. From Qiskit program to internal IR. The user specifies a circuit via the Qiskit Python API. Qiskit lowers it to a QuantumCircuit object, which is both its internal IR and the entry point to QSeqSim. Parser (compile phase). Given a QuantumCircuit, the Parser performs the following steps: 1. OpenQASM 3 export. We invoke Qiskit’s qasm3.dumps routine to obtain an external IR in the form of an… view at source ↗
Figure 3
Figure 3. Figure 3: Circuit-level view of one SQC iteration (composition, dynamic body with [PITH_FULL_IMAGE:figures/full_fig_p021_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A SQC for the Repeat-Until-Success protocol of implementing [PITH_FULL_IMAGE:figures/full_fig_p025_4.png] view at source ↗
read the original abstract

We present a tool QSeqSim, a Qiskit-integrated symbolic backend that fills the current gap of having no Qiskit-native support for simulating while-loop quantum programs and their induced sequential quantum circuits. QSeqSim takes Qiskit QuantumCircuit objects, translates them into OpenQASM 3 code, and organises the resulting program into a combination of combinational, dynamic, and sequential circuits, thereby assigning while-loops a precise sequential circuit semantics with explicit internal and external qubits. Building on this semantics, QSeqSim adopts a Binary Decision Diagram (BDD)-based symbolic representation and integrates weighted model counting to compute measurement probabilities efficiently by exploiting sharing in structured and sparse BDDs. On top of this Boolean backbone, it introduces dedicated symbolic operators for state composition and state retention, thereby enabling efficient symbolic execution of sequential quantum circuits. Our experiments demonstrate that QSeqSim scales to substantial while-induced sequential circuits; in particular, in the quantum random walk benchmark we successfully simulate circuits with over 1000 qubits for more than 10 loop iterations. QSeqSim is available at https://github.com/Veri-Q/QSeqSim.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper presents QSeqSim, a Qiskit-integrated symbolic backend for simulating while-loop quantum programs. It translates QuantumCircuit objects to OpenQASM 3, assigns while-loops explicit sequential circuit semantics with internal/external qubits, employs BDD-based symbolic representation with weighted model counting, and introduces dedicated operators for state composition and retention. Experiments claim successful simulation of while-induced sequential circuits, notably a quantum random walk with >1000 qubits over >10 iterations.

Significance. If the dedicated symbolic operators for composition and retention preserve structured and sparse BDD representations without exponential blowup, the tool would address a genuine gap in native Qiskit support for looped quantum programs and enable more efficient symbolic execution than standard simulation approaches. Open-source release on GitHub adds practical value for the community.

major comments (1)
  1. [Abstract] Abstract (and Experiments section): the central scaling claim that QSeqSim 'scales to substantial while-induced sequential circuits' rests on a single structured benchmark (quantum random walk); no BDD node counts, growth rates, or results on other while-loop circuit families are reported to test when the structure-preserving property of the composition/retention operators holds versus when exponential blowup occurs.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback on the scaling claims. Below we respond point-by-point to the major comment.

read point-by-point responses

  1. Referee: [Abstract] Abstract (and Experiments section): the central scaling claim that QSeqSim 'scales to substantial while-induced sequential circuits' rests on a single structured benchmark (quantum random walk); no BDD node counts, growth rates, or results on other while-loop circuit families are reported to test when the structure-preserving property of the composition/retention operators holds versus when exponential blowup occurs.

    Authors: We agree that the experimental evaluation centers on the quantum random walk as the primary benchmark. This choice reflects its status as a standard example of while-loop programs that induce sequential quantum circuits requiring repeated state retention and composition. The reported scaling to >1000 qubits over >10 iterations demonstrates that the dedicated operators can preserve structured BDD representations in this structured case. However, the manuscript does not provide BDD node counts, growth rates, or results on additional while-loop families that would delineate the boundary between structure preservation and potential blowup. We will revise the Experiments section to include these metrics and results from further circuit families, thereby strengthening the evidence for the conditions under which the operators remain efficient. revision: yes

Circularity Check

0 steps flagged

No circularity: implementation of a new simulator tool with benchmark results

full rationale

The paper presents QSeqSim as a software tool that translates Qiskit circuits to OpenQASM 3, assigns sequential semantics to while-loops, and implements BDD-based symbolic simulation with custom operators for composition and retention. The scaling claim rests on experimental results from the quantum random walk benchmark rather than any derivation that reduces to its own fitted parameters or self-citations. No load-bearing step equates a prediction to an input by construction, imports uniqueness via self-citation, or renames a known result; the work is self-contained as an engineering artifact whose tractability claims are externally falsifiable via the released code and additional benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper relies on standard mathematical properties of BDDs and model counting, as well as the Qiskit and OpenQASM frameworks, without additional free parameters or invented entities beyond the tool itself.

pith-pipeline@v0.9.1-grok · 5736 in / 1158 out tokens · 35255 ms · 2026-06-30T20:06:02.584840+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 6 canonical work pages · 3 internal anchors

  1. [1]

    Journal of the ACM (JACM)62(1), 1–34 (2015)

    Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.: Approximate verification of the symbolic dynamics of markov chains. Journal of the ACM (JACM)62(1), 1–34 (2015)

    2015

  2. [2]

    Information Processing Letters115(2), 155–158 (2015)

    Akshay, S., Antonopoulos, T., Ouaknine, J., Worrell, J.: Reachability problems for markov chains. Information Processing Letters115(2), 155–158 (2015)

    2015

  3. [3]

    Quantum Science & Technology7(2), 025007 (2022)

    Andrés-Martínez, P., Heunen, C.: Weakly measured while loops: peeking at quan- tum states. Quantum Science & Technology7(2), 025007 (2022)

    2022

  4. [4]

    In: International Workshop on Computer Science Logic

    Beauquier, D., Rabinovich, A., Slissenko, A.: A logic of probability with decidable model-checking. In: International Workshop on Computer Science Logic. pp. 306–

  5. [5]

    Physical review letters114(8), 080502 (2015)

    Bocharov, A., Roetteler, M., Svore, K.M.: Efficient synthesis of universal repeat- until-success quantum circuits. Physical review letters114(8), 080502 (2015)

    2015

  6. [6]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810–1824 (2020)

    Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810–1824 (2020)

    2020

  7. [7]

    Artificial Intelligence172(6-7), 772–799 (2008)

    Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artificial Intelligence172(6-7), 772–799 (2008)

    2008

  8. [8]

    In: International Conference on Tools and Algo- rithms for the Construction and Analysis of Systems

    Chen, T.F., Jiang, J.H.R.: SliQSim: A quantum circuit simulator and solver for probability and statistics queries. In: International Conference on Tools and Algo- rithms for the Construction and Analysis of Systems. pp. 129–138. Springer (2025)

    2025

  9. [9]

    In: International Conference on Tools and Algorithms for the Construc- tion and Analysis of Systems

    Chen, Y.F., Chung, K.M., Hsieh, M.H., Huang, W.J., Lengál, O., Lin, J.A., Tsai, W.L.: AutoQ 2.0: From verification of quantum circuits to verification of quantum programs. In: International Conference on Tools and Algorithms for the Construc- tion and Analysis of Systems. pp. 87–108. Springer (2025)

    2025

  10. [10]

    In: International Conference on Computer Aided Verification

    Chen, Y.F., Chung, K.M., Lengál, O., Lin, J.A., Tsai, W.L.: AutoQ: An automata- based quantum circuit verifier. In: International Conference on Computer Aided Verification. pp. 139–153. Springer (2023) QSeqSim 19

    2023

  11. [11]

    Proceedings of the ACM on Programming Languages7(PLDI), 1218–1243 (2023)

    Chen, Y.F., Chung, K.M., Lengál, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. Proceedings of the ACM on Programming Languages7(PLDI), 1218–1243 (2023)

    2023

  12. [12]

    https://doi.org/10.5281/zenodo

    Cirq Developers: Cirq (v1.6.1) (2025).https://doi.org/10.5281/zenodo. 16867504

    work page doi:10.5281/zenodo 2025

  13. [13]

    ACM Transactions on Quantum Computing3(3), 1–50 (2022)

    Cross, A., Javadi-Abhari, A., Alexander, T., De Beaudrap, N., Bishop, L.S., Heidel, S., Ryan, C.A., Sivarajah, P., Smolin, J., Gambetta, J.M., et al.: OpenQASM 3: A broader and deeper quantum assembly language. ACM Transactions on Quantum Computing3(3), 1–50 (2022)

    2022

  14. [14]

    Physical review letters108(26), 260501 (2012)

    Eisert, J., Müller, M.P., Gogolin, C.: Quantum measurement occurrence is unde- cidable. Physical review letters108(26), 260501 (2012)

    2012

  15. [15]

    Journal of Computer and System Sciences79(7), 1181–1198 (2013)

    Feng, Y., Yu, N., Ying, M.: Model checking quantum markov chains. Journal of Computer and System Sciences79(7), 1181–1198 (2013)

    2013

  16. [16]

    Probabilistic Model--Checking of Quantum Protocols

    Gay, S., Nagarajan, R., Papanikolaou, N.: Probabilistic model–checking of quan- tum protocols. arXiv preprint quant-ph/0504007 (2005)

    work page internal anchor Pith review Pith/arXiv arXiv 2005

  17. [17]

    Digitale Welt5(2), 14–17 (2021)

    Gonzalez, C.: Cloud based QC with Amazon Braket. Digitale Welt5(2), 14–17 (2021)

    2021

  18. [18]

    In: Pro- ceedings of the twenty-eighth annual ACM symposium on Theory of computing

    Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Pro- ceedings of the twenty-eighth annual ACM symposium on Theory of computing. pp. 212–219 (1996)

    1996

  19. [19]

    In: International Conference on Computer Aided Verification

    Guan, J., Feng, Y., Turrini, A., Ying, M.: Measurement-based verification of quan- tum markov chains. In: International Conference on Computer Aided Verification. pp. 533–554. Springer (2024)

    2024

  20. [20]

    Quantum Science & Technology5(3), 034007 (2020)

    Guerreschi, G.G., Hogaboam, J., Baruffa, F., Sawaya, N.P.: Intel Quantum Sim- ulator: A cloud-ready high-performance simulator of quantum circuits. Quantum Science & Technology5(3), 034007 (2020)

    2020

  21. [21]

    John Wiley & Sons (2000)

    Hoaglin, D.C., Mosteller, F., Tukey, J.W.: Understanding robust and exploratory data analysis. John Wiley & Sons (2000)

    2000

  22. [22]

    Quantum computing with Qiskit

    Javadi-Abhari, A., Treinish, M., Krsulich, K., Wood, C.J., Lishman, J., Gacon, J., Martiel, S., Nation, P.D., Bishop, L.S., Cross, A.W., et al.: Quantum computing with Qiskit. arXiv preprint arXiv:2405.08810 (2024)

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  23. [23]

    Scientific reports9(1), 10736 (2019)

    Jones, T., Brown, A., Bush, I., Benjamin, S.C.: QuEST and high performance simulation of quantum computers. Scientific reports9(1), 10736 (2019)

    2019

  24. [24]

    Physical Review A67(4), 042315 (2003)

    Kendon, V., Tregenna, B.: Decoherence can be useful in quantum walks. Physical Review A67(4), 042315 (2003)

    2003

  25. [25]

    arXiv preprint arXiv:1904.04735 (2019)

    Kissinger, A., Van De Wetering, J.: PyZX: Large scale automated diagrammatic reasoning. arXiv preprint arXiv:1904.04735 (2019)

    work page arXiv 1904

  26. [26]

    In: International conference on computer aided verification

    Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using quantum hoare logic. In: International conference on computer aided verification. pp. 187–207. Springer (2019)

    2019

  27. [27]

    In: International Conference on Computer Aided Verification

    Mei,J.,Bonsangue,M.,Laarman,A.:Simulatingquantumcircuitsbymodelcount- ing. In: International Conference on Computer Aided Verification. pp. 555–578. Springer (2024)

    2024

  28. [28]

    In: International Joint Conference on Automated Reasoning

    Mei,J.,Coopmans,T.,Bonsangue,M.,Laarman,A.:Equivalencecheckingofquan- tum circuits by model counting. In: International Joint Conference on Automated Reasoning. pp. 401–421. Springer (2024)

    2024

  29. [29]

    com/index.html(2025), accessed: 2026-03-02

    OpenQASM Contributors: OpenQASM Live Specification.https://openqasm. com/index.html(2025), accessed: 2026-03-02

    2025

  30. [30]

    Repeat-Until-Success: Non-deterministic decomposition of single-qubit unitaries

    Paetznick, A., Svore, K.M.: Repeat-until-success: Non-deterministic decomposition of single-qubit unitaries. arXiv preprint arXiv:1311.1074 (2013) 20 Z. Li et al

    work page internal anchor Pith review Pith/arXiv arXiv 2013

  31. [31]

    Papanikolaou, N.K.: Model checking quantum protocols. Ph.D. thesis, University of Warwick (2009)

    2009

  32. [32]

    IEEE Journal on Emerging and Selected Topics in Circuits and Systems12(3), 662–675 (2022)

    Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of quantum circuits with the zx-calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems12(3), 662–675 (2022)

    2022

  33. [33]

    In: International Symposium on Formal Methods

    Quist, A.J., Mei, J., Coopmans, T., Laarman, A.: Advancing quantum computing with formal methods. In: International Symposium on Formal Methods. pp. 420–

  34. [34]

    Mathematical Structures in Computer Science14(4), 527–586 (2004)

    Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science14(4), 527–586 (2004)

    2004

  35. [35]

    Physical Review A67(5), 052307 (2003)

    Shenvi, N., Kempe, J., Whaley, K.B.: Quantum random-walk search algorithm. Physical Review A67(5), 052307 (2003)

    2003

  36. [36]

    Quantum2, 49 (2018)

    Steiger, D.S., Häner, T., Troyer, M.: ProjectQ: an open source software framework for quantum computing. Quantum2, 49 (2018)

    2018

  37. [37]

    Quantum5, 559 (2021)

    Suzuki, Y., Kawase, Y., Masumura, Y., Hiraga, Y., Nakadai, M., Chen, J., Nakan- ishi, K.M., Mitarai, K., Imai, R., Tamiya, S., et al.: Qulacs: a fast and versatile quantum circuit simulator for research purpose. Quantum5, 559 (2021)

    2021

  38. [38]

    The CUDA Quantum development team: CUDA Quantum (0.11.0) (2025).https: //doi.org/10.5281/zenodo.15407754

    work page doi:10.5281/zenodo.15407754 2025

  39. [39]

    In: 2021 58th ACM/IEEE Design Automation Conference (DAC)

    Tsai, Y.H., Jiang, J.H.R., Jhang, C.S.: Bit-slicing the hilbert space: Scaling up ac- curate quantum circuit simulation. In: 2021 58th ACM/IEEE Design Automation Conference (DAC). pp. 439–444. IEEE (2021)

    2021

  40. [40]

    Proceedings of the ACM on Program- ming Languages3(POPL), 1–31 (2019)

    Unruh, D.: Quantum relational hoare logic. Proceedings of the ACM on Program- ming Languages3(POPL), 1–31 (2019)

    2019

  41. [41]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41(9), 3143–3156 (2021)

    Wang, Q., Li, R., Ying, M.: Equivalence checking of sequential quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41(9), 3143–3156 (2021)

    2021

  42. [42]

    In: International Conference on Computer Aided Ver- ification

    Wang, Z., Cheng, B., Yuan, L., Ji, Z.: Feynmandd: Quantum circuit analysis with classical decision diagrams. In: International Conference on Computer Aided Ver- ification. pp. 28–52. Springer (2025)

    2025

  43. [43]

    In: Proceedings of the 59th ACM/IEEE Design Automation Conference

    Wei, C.Y., Tsai, Y.H., Jhang, C.S., Jiang, J.H.R.: Accurate bdd-based unitary operator manipulation for scalable and robust quantum circuit verification. In: Proceedings of the 59th ACM/IEEE Design Automation Conference. pp. 523–528 (2022)

    2022

  44. [44]

    ACM Transactions on Pro- gramming Languages and Systems (TOPLAS)33(6), 1–49 (2012)

    Ying, M.: Floyd–hoare logic for quantum programs. ACM Transactions on Pro- gramming Languages and Systems (TOPLAS)33(6), 1–49 (2012)

    2012

  45. [45]

    In: International Symposium on Formal Methods

    Ying, M.: Model checking for verification of quantum circuits. In: International Symposium on Formal Methods. pp. 23–39. Springer (2021)

    2021

  46. [46]

    Elsevier (2024)

    Ying, M.: Foundations of quantum programming. Elsevier (2024)

    2024

  47. [47]

    Acta Informatica47(4), 221–250 (2010)

    Ying, M., Feng, Y.: Quantum loop programs. Acta Informatica47(4), 221–250 (2010)

    2010

  48. [48]

    In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

    Zhou, L., Yu, N., Ying, M.: An applied quantum hoare logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 1149–1162 (2019)

    2019

  49. [49]

    Zulehner, A., Wille, R.: Advanced simulation of quantum computations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems38(5), 848–859 (2018) QSeqSim 21 A Overview This appendix records lemmas on the(k,{F i x})encoding that justify thestate compositionandstate retentionsteps in Algorithm 2, together with the mid- circuit measure...

    2018