REVIEW
When Equivalent Quantum Circuits Lose Synthesis Choices
Quantum Physics · Submitted 5 Oct 2026 · 53 references
Pith's verdict: OpenQASM round trips silently kill synthesis availability with every oracle passing — the measurement work is solid, but Verified's recovery envelope is the ≤10-qubit regime by construction, not just as an untested scaling limit.
T0 · AI review
Why Pith says this
Highlight any text to comment on it.
Referee report
The paper
The paper claims
A quantum circuit can pass every functional-equivalence oracle and still silently lose its intended optimization when moved across an OpenQASM boundary, and a verified operation record can put that synthesis choice back.
The reading
What carries the argument
The central object is synthesis availability, defined as the receiving compiler being able to apply a synthesis method directly to a high-level operation in the delivered representation, and the paper's measure of success is whether the requested method both gets invoked and returns a synthesis circuit. The recovery machinery is the operation record, which stores an operation's type, parameters, and qubit binding together with a SHA-256 fingerprint of the region's QPY serialization, read by a three-stage procedure (Locate, Verify, Reconstruct). Verify uses the fingerprint as a fast path and falls back to a bounded operator-equivalence check that constructs dense matrices of size $O(4^n)$, applied only up to ten qubits, with regions above that size accepted only on an exact fingerprint match. The load-bearing distinction is between a valid record, where the region remains identifiable and reconstruction is functionally equivalent, and a stale record, where routing, optimization, or approximate recompilation has changed the region; Verified reconstructs only after the check passes, which is what prevents non-equivalent circuits, at the cost of also rejecting some valid records.
Extended reading notes
Core claim
The central claim is that preserving computation is not the same as preserving the compiler's ability to synthesize, and that a functionally equivalent circuit can silently lose its intended optimization. The paper demonstrates this with a ten-qubit QFT on a linear target: a direct OpenQASM 3 round trip keeps the computation but turns the QFTGate into a generic Gate named qft; Qiskit's dispatch still invokes the requested method qft.line, yet the method requires a QFTGate and returns no synthesis circuit for the generic object, so compilation proceeds from the imported gate definition and the median two-qubit count rises from 135 to 150. This is not a QFT quirk: 52 of the 55 registered synthesis entry points across 14 operation families check the delivered object's type and produce a circuit only for the expected type, so the silent no-op generalizes. Across the request study, the direct OpenQASM 3 round trip delivers 360 eligible conditions, and in every one the requested method is invoked, receives a generic Gate, returns nothing, and compilation still succeeds for all ten routing seeds with no exception or warning. The companion result is that Verified restores the requested synthesis in all 830 recovery runs, matching the original compilation exactly in two-qubit count and depth, while rejecting every stale record in the evaluated sets; unchecked reconstruction from a stale record produces a non-equivalent circuit in all 17 such cases tested.
Load-bearing premise
Verified's reconstruction guarantee rests on the bounded operator-equivalence check, which uses dense matrices and applies only up to ten qubits; above that size, any representation change alters the SHA-256 fingerprint, so no record for a larger region survives a changed representation, meaning Verified currently guarantees safety only for small circuits, and for those only if the shared equivalence check itself is correct.
Editorial extensions
If this is right
- Compiler developers should report whether a requested synthesis method is invoked, whether it produces a circuit, and whether that circuit is applied, because silent no-op synthesis is currently possible in Qiskit's HLS dispatch.
- Interchange tools that cannot preserve a high-level operation should retain a verified operation record, since reconstruction from an unverified record can change the circuit's computation.
- Researchers should report the representation supplied to the compiler along with workload and settings, because functionally equivalent representations can differ in synthesis availability and therefore in compiled cost.
- Preserving the high-level operation keeps synthesis choices available but does not guarantee a cheaper circuit; the benefit of MCX synthesis depends on available clean ancillas and the benefit for adders on adder size.
Reading between the lines
- The paper's audit found no HLSConfig request in the project corpus that crossed a representation change, so the 360-condition silent-no-op result is controlled-experiment evidence rather than a measured prevalence; how often real pipelines hit this pattern remains unquantified.
- Verified's practical reach today is small circuits: the bounded equivalence check stops at ten qubits, and the SHA-256 fingerprint changes in all 830 recovery runs, so any region larger than ten qubits that undergoes any representation change is rejected outright rather than recovered.
- A portable, non-dense equivalence oracle would be the enabling step the paper leaves open: storing operation records in OpenQASM 3 directives (listed as future work) would only help if the check itself scales past ten qubits.
- A testable consequence for the broader toolchain is that any compiler reporting 'synthesis applied' without confirming the method produced a circuit can be audited by inspecting dispatch return values; the paper's finding that 52 of 55 entry points type-check suggests the failure mode is a design property, not a single-version bug.
Original abstract
Quantum compilers synthesize high-level operations, such as the quantum Fourier transform and multi-controlled X gates, into gate-level circuits. Across compilation stages, a circuit may be serialized, exchanged as OpenQASM, converted between compilers, or lowered to gates. These representation changes can preserve computation while removing the high-level operation itself, leaving the receiving compiler unable to apply a requested synthesis method. We call this loss synthesis availability. We study synthesis availability in Qiskit, TKET, and Cirq through controlled experiments, repository analysis, circuits captured from project tests, and a Munich Quantum Toolkit pipeline. Synthesis availability survives serialization when deserialization restores the high-level operation and survives compiler conversion only when the receiving compiler supports that operation. It does not survive the evaluated OpenQASM routes. After a direct OpenQASM 3 round trip, requested synthesis has no effect in all 360 delivered conditions even though compilation succeeds. In the MQT pipeline, OpenQASM 2 interchange increases the two-qubit gate count by 37.2 percent for an eight-qubit Grover circuit. We also introduce Verified, which records high-level operations before a representation change and reconstructs them only when a check confirms that the record still matches the delivered circuit. Verified restores requested synthesis in all 830 recovery runs, with median verification times from 2.0 to 638 ms per operation family. The check rejects every stale record but also some valid records. These results show that preserving functional equivalence alone is insufficient when later synthesis choices depend on retained high-level structure.
The compiled record
The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
The abstract, sentence by sentence
Quantum compilers synthesize high-level operations, such as the quantum Fourier transform and multi-controlled X gates, into gate-level circuits. Across compilation stages, a circuit may be serialized, exchanged as OpenQASM, converted between compilers, or lowered to gates. These representation changes can preserve computation while removing the high-level operation itself, leaving the receiving compiler unable to apply a requested synthesis method. We call this loss synthesis availability. We study synthesis availability in Qiskit, TKET, and Cirq through controlled experiments, repository analysis, circuits captured from project tests, and a Munich Quantum Toolkit pipeline. Synthesis availability survives serialization when deserialization restores the high-level operation and survives compiler conversion only when the receiving compiler supports that operation. It does not survive the evaluated OpenQASM routes. After a direct OpenQASM 3 round trip, requested synthesis has no effect in all 360 delivered conditions even though compilation succeeds. In the MQT pipeline, OpenQASM 2 interchange increases the two-qubit gate count by 37.2 percent for an eight-qubit Grover circuit. We also introduce Verified, which records high-level operations before a representation change and reconstructs them only when a check confirms that the record still matches the delivered circuit. Verified restores requested synthesis in all 830 recovery runs, with median verification times from 2.0 to 638 ms per operation family. The check rejects every stale record but also some valid records. These results show that preserving functional equivalence alone is insufficient when later synthesis choices depend on retained high-level structure.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | Quantum compilers synthesize high-level operations, such as the quantum Fourier transform and multi-controlled X gates, into gate-level circuits. | background 1.00 | 0.05 | 0.02 | asserted 1.00 |
| s1 | Across compilation stages, a circuit may be serialized, exchanged as OpenQASM, converted between compilers, or lowered to gates. | background 1.00 | 0.07 | 0.02 | hedged possibility 0.97 |
| s2 | These representation changes can preserve computation while removing the high-level operation itself, leaving the receiving compiler unable to apply a requested synthesis method. | background 0.95 | 0.12 | 0.16 | hedged possibility 0.66 |
| s3 | We call this loss synthesis availability. | contribution 0.47 | 0.43 | 0.04 | asserted 0.85 |
| s4 | We study synthesis availability in Qiskit, TKET, and Cirq through controlled experiments, repository analysis, circuits captured from project tests, and a Munich Quantum Toolkit pipeline. | method 0.84 | 0.95 | 0.03 | asserted 0.91 |
| s5 | Synthesis availability survives serialization when deserialization restores the high-level operation and survives compiler conversion only when the receiving compiler supports that operation. | result 0.99 | 0.90 | 0.22 | asserted 1.00 |
| s6 | It does not survive the evaluated OpenQASM routes. | result 1.00 | 0.88 | 0.13 | asserted 1.00 |
| s7 | After a direct OpenQASM 3 round trip, requested synthesis has no effect in all 360 delivered conditions even though compilation succeeds. | result 1.00 | 0.94 | 0.11 | asserted 1.00 |
| s8 | In the MQT pipeline, OpenQASM 2 interchange increases the two-qubit gate count by 37.2 percent for an eight-qubit Grover circuit. | result 1.00 | 0.94 | 0.04 | asserted 1.00 |
| s9 | We also introduce Verified, which records high-level operations before a representation change and reconstructs them only when a check confirms that the record still matches the delivered circuit. | contribution 0.78 | 0.94 | 0.06 | asserted 0.99 |
| s10 | Verified restores requested synthesis in all 830 recovery runs, with median verification times from 2.0 to 638 ms per operation family. | result 0.99 | 0.96 | 0.09 | asserted 1.00 |
| s11 | The check rejects every stale record but also some valid records. | limitation 0.67 | 0.94 | 0.06 | asserted 1.00 |
| s12 | These results show that preserving functional equivalence alone is insufficient when later synthesis choices depend on retained high-level structure. | interpretation 1.00 | 0.83 | 0.90 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
Figures
Figures reproduced from arXiv:2610.06142 by the authors.
References
Discussion
Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.