Optimising Clifford Circuits with Quantomatic
We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Clifford Circuits can be Properly PAC Learned if and only if $\textsf{RP}=\textsf{NP}$
Given a dataset of input states, measurements, and probabilities, is it possible to efficiently predict the measurement probabilities associated with a quantum circuit? Recent work of Caro and Datta (2020) studied the pr…
Computational EfficiencyPAC learningEquivariant Reinforcement Learning for Clifford Quantum Circuit Synthesis
We consider the problem of synthesizing Clifford quantum circuits for devices with all-to-all qubit connectivity. We approach this task as a reinforcement learning problem in which an agent learns to discover a sequence …
Reinforcement LearningAlphaClifford: Efficient Clifford Synthesis and Transpilation with Model-based RL
Clifford circuits play a foundational role in quantum computing, particularly due to their importance in quantum error correction and fault-tolerant logical synthesis. While these circuits can be efficiently simulated an…
Reinforcement LearningVerifying the Steane code with Quantomatic
In this paper we give a partially mechanized proof of the correctness of Steane's 7-qubit error correcting code, using the tool Quantomatic. To the best of our knowledge, this represents the largest and most complicated …
When Close Enough Is Not Enough: Autoregressive Drift in Quantum Circuit Synthesis
Quantum circuit optimization for fault-tolerant computing requires exact functional equivalence while minimizing expensive non-Clifford resources such as T gates. We study this problem using a compact 44.8M-parameter enc…