It is proved that the local ZX simplification layer (spider fusion and identity removal) computes exactly the free-product normal form of Z_2 * Z_8, giving exact per-instance compression and, under a calibrated ergodicity hypothesis, a depth-independent limit law confirmed on two independently constructed nets.
Abstract
Gate synthesis and circuit optimization are usually studied separately, and evidence on their interaction is contradictory: ZX-calculus rewriting removes a stable fraction of Solovay-Kitaev circuits, yet almost nothing from number-theoretically synthesized circuits. We show both behaviours follow from a single bound. For any optimizer that preserves the implemented element exactly--including all sound ZX rewriting with extraction--the achievable T-count is bounded below by the denominator exponent of the synthesized ring element. This exactness barrier is computable per instance and separates exact post-processing from approximation-aware resynthesis by a certified factor reaching 101x at recursion depth five. The two behaviours are then the barrier operating at different distances from the floor. For Solovay-Kitaev circuits we prove that the local ZX simplification layer (spider fusion and identity removal) computes exactly the free-product normal form of Z_2 * Z_8, giving exact per-instance compression and, under a calibrated ergodicity hypothesis, a depth-independent limit law confirmed on two independently constructed nets. For number-theoretically synthesized circuits the floor is already saturated: on single-qubit words automated ZX simplification attains it exactly, via a closed-form formula for minimal T-count in terms of phase linkage through the Z-axis normalizer. At two qubits and beyond the same valuation yields unconditional rigidity certificates, which on the quantum-Shannon-decomposition plus gridsynth pipeline certify 99.4-99.9% of the synthesized T-count as incompressible, with rigidity strengthening as accuracy tightens. This explains, and predicts the size of, the near-null optimization recently reported for that pipeline.
A measurement of what diagrammatic post-processing recovers from structural redundancy in the Solovay-Kitaev algorithm, which optimizes for numerical convergence rather than circuit economy, and its output carries structural redundancy that a gate-level compiler cannot see.
Dulari De Silva, A. Mahasinghe, Chon-Fai Kam et al.· 0 citations
A unified, highly scalable methodology for the optimal design of reversible circuits across both libraries is presented, establishing best-known upper bounds that significantly outperform heuristic literature benchmarks.
Minimizing the number of CNOT gates required to synthesize a Clifford operator is a central problem in quantum circuit optimization. We extend the link--middle--cut (LMC) framework for linear reversible circuits to Clifford operators represented by binary symplectic tableaux. By introducing block-support connectivity graphs and determinantal invariants, we obtain efficiently computable lower bounds on ancilla-free CNOT complexity. We prove that these bounds are tight for qubit permutations: a permutation of $n$ qubits with $k$ cycles requires exactly $3(n-k)$ CNOT gates, even when arbitrary one-qubit Clifford gates are available. We also derive efficiently computable bounds for synthesis up to a permutation of the output qubits, corresponding to free qubit relabeling. Finally, we further demonstrate the utility of the bound by using it as an admissible heuristic for $A^*$-based Clifford synthesis and show that, on benchmark instances, the resulting search can prove optimality beyond what was possible with earlier SAT-based methods, and that it may be used in combination with earlier $A^*$ heuristics to improve the CNOT counts obtained through heuristic search.
In fault-tolerant quantum computing, lattice surgery (LS) is one of the leading ways to realize logical operations, and the Pauli product measurement (PPM) is the basic instruction of LS-based computing. Compilers on the PPM sequence, however, stay at the logical level rather than the physical circuit level. This is because the lowering is complicated: PPMs differ widely from each other, and each must be realized on the physical circuit without breaking fault tolerance. CircLS lowers the PPM sequence to a Stim circuit through linear-time stabilizer construction rules. This completes the pipeline from a quantum program through the PPM sequence to a Stim circuit, on which the compiled program can be verified at the circuit level and its logical error rate (LER) measured. Based on the lowering, we develop a compiler that allocates data patches dynamically: each patch is allocated at its first use and freed at its last use, and the freed tiles are reused as ancilla paths. CircLS reduces the allocated spacetime volume by $5.5\times$ and the LER by $14\times$ against the prior toolchain producing runnable circuits. CircLS is open source at https://github.com/John-YuehanZhang/CircLS.
We present AlchemQ v0.5, a proof-of-concept system that couples an untrusted beam-search optimizer with a machine-checkable per-result certification layer and a versioned certificate protocol (0.2.0), so that every optimized circuit ships with a verifiable artifact rather than a bare claim. The certifier proves equivalence up to global phase by ZX-calculus full reduction, with a numeric-tensor fallback based on the optimal Hilbert-Schmidt overlap. Certificates are self-contained and tamper-evident: canonical gate-canon-v1 hashes, measured residuals, tri-state verdicts (certified/rejected/inconclusive), and versioned phase-note schemas for cross-platform reproducibility. The agent aggregates three fuzzy t-norms, cannot return an uncertified circuit, and since v0.4 guarantees no componentwise regression against the original. On a benchmark of 100 circuits, all 400 optimizations terminate without error, every returned circuit is certified, every mutation is detected, and a 2998-test suite passes on two platforms. The PyZX baseline is strong (21.4% mean T-count reduction over 82 circuits) and the agent is strictly better on 9/100; the three t-norms return identical circuits on all 100 standard instances, diverging only on 4/38 of an adversarial suite. Two case studies are new: a false negative root-caused to a pivot-normalization bug in PyZX's compare_tensors (pivot 4.7e-9; the optimal-overlap residual is 7.4e-11), and eight certificates rejected on macOS due to BLAS-dependent floats in phase_note. Both were fixed; all artifact sets validate 400/400 on both platforms. A pilot run on IBM Heron r2 gives a certified circuit 78% shallower with 65% fewer two-qubit gates; output quality favors it on all three metrics but is not significant at 1024 shots. We release the certificate specification and a standalone reference verifier (Apache-2.0) with data and scripts; the engine is proprietary.
We describe Renesis, an automated synthesis tool that accepts an ordinary irreversible netlist and produces a verified, technology-mapped energy-recovery (adiabatic) circuit, using energy rather than area or delay as the optimization criterion. Renesis models the netlist with a vector-space formulation that expresses simulation and justification sweeps as forward and reverse traversals whose cost is linear in the number of circuit components. The traversals populate ledgers with data tags that characterize switching, erasure, and observability information at their natural R\'enyi orders. The output is a logically reversible circuit mapped to one of eight energy-recovery families, with the associated parameters reported. Reversibility is treated here as a circuit-level requirement rather than a thermodynamic one. When an adiabatic gate erases information the penalty is not $k_B T \ln 2$ but a full non-adiabatic $CV^2$ discharge, which is comparable to the switching energy the circuit style exists to recover. Every synthesis transformation is equivalence-checked, and it must improve one of two reported cost tables, one uncapped and one after a series-realizability bound, while worsening neither before it is accepted. Across a twenty-circuit development set, optional re-synthesis passes improve fourteen circuits. On a held-out set of twenty circuits, fifteen of nineteen are improved, with a best-arm median of $0.91$ of the default energy. A certified optimality-gap program computes the distance between the synthesized circuits and the provable floor of the tool's own search space. A device-level SPICE deck reproduces the tool's per-cycle energy figures on the reference family. The tool, the benchmark netlists, the validation procedure, and the run records behind every reported number are released as open source.
Mitchell A. Thornton· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
