Ensuring ancilla safety is a critical correctness requirement for quantum compilation, since ancilla qubits are routinely introduced to implement complex operations with fewer gates and reduced depth. However, formally verifying this property is computationally hard due to state-space explosion in the number of qubits, particularly for dirty ancillae, which carry unknown initial states and must be restored after use. We propose an end-to-end verification-and-repair framework that rigorously addresses both clean and dirty ancilla safety. Our core contribution is a two-step reduction strategy: we first prove that verifying an $m$-qubit dirty ancilla register decomposes into $2m$ independent clean ancilla safety checks; subsequently, we reduce each clean ancilla safety instance to an algebraic commutativity check against Pauli-$Z$ and Pauli-$X$ operators. This approach yields an efficient and naturally parallel verifier and enables actionable diagnosis by classifying violations into logic errors and phase errors. Leveraging this diagnosis, we further design lightweight repair routines that append local single-qubit rotations to eliminate a broad class of local ancilla faults. We implement the full pipeline in a prototype tool using a dual-backend architecture combining decision diagrams and weighted model counting, and validate it on diverse circuits ranging from arithmetic benchmarks to Grover's algorithm. Our experiments demonstrate scalability to thousands of qubits and show that the proposed repairs effectively improve ancilla safety while preserving circuit functionality.
Jiqi Li, Jingyi Mei, Wang Fang et al.· International Conference on...· 1 citation
The state frame potential is a standard diagnostic of how closely a quantum state ensemble approximates Haar randomness. In this work, we study the problem of estimating the state frame potential of order $t$ to within additive error $\varepsilon$ under three progressively weaker access models: (i) query access to a multi-state-preparation oracle, (ii) general sample access, and (iii) single-copy sample access. In the query model, we establish a near-optimal query complexity of $\widetilde{\Theta}(\sqrt{t}/\varepsilon)$, yielding a quadratic improvement in the dependence on $t$ over the previous best result of Nakata, Takeuchi, Kliesch, and Darmawan (PRX Quantum 2025). In the general sample model, we establish the optimal sample complexity $\Theta(t/\varepsilon^2)$. In the single-copy sample model, we present a store-and-estimate approach whose sample complexity depends on the R\'enyi entropy of the ensemble weights. As an application, we use the single-copy algorithm to assess the randomness of projected state ensembles, where the entropy term becomes the observational R\'enyi entropy associated with measuring one subsystem.
Jing Bao, Wang Fang, Y. Nakata et al.· 0 citations
SymFT, a high-throughput simulator for Clifford-dominated circuits with Pauli rotations, stochastic Pauli noise, mid-circuit Pauli measurements, and measurement-record-controlled Pauli feedback, achieves state-of-the-art sampling performance.