-
Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits (Extended)
Authors:
Neil J. Ross,
Scott Wesley
Abstract:
Many promising quantum algorithms in economics, medical science, and material science rely on circuits that are parameterized by a large number of angles. To ensure that these algorithms are efficient, these parameterized circuits must be heavily optimized. However, most quantum circuit optimizers are not verified, so this procedure is known to be error-prone. For this reason, there is growing int…
▽ More
Many promising quantum algorithms in economics, medical science, and material science rely on circuits that are parameterized by a large number of angles. To ensure that these algorithms are efficient, these parameterized circuits must be heavily optimized. However, most quantum circuit optimizers are not verified, so this procedure is known to be error-prone. For this reason, there is growing interest in the design of equivalence checking algorithms for parameterized quantum circuits. In this paper, we define a generalized class of parameterized circuits with arbitrary rotations and show that this problem is decidable for cyclotomic gate sets. We propose a cutoff-based procedure which reduces the problem of verifying the equivalence of parameterized quantum circuits to the problem of verifying the equivalence of finitely many parameter-free quantum circuits. Because the number of parameter-free circuits grows exponentially with the number of parameters, we also propose a probabilistic variant of the algorithm for cases when the number of parameters is intractably large. We show that our techniques extend to equivalence modulo global phase, and describe an efficient angle sampling procedure for cyclotomic gate sets.
△ Less
Submitted 7 July, 2025; v1 submitted 25 June, 2025;
originally announced June 2025.
-
Enriched Categories for Parameterized Circuit Semantics
Authors:
Scott Wesley
Abstract:
It is well-known that combinatorial circuits are modeled mathematically by string diagrams in a monoidal category. Given a gate set $Σ$, the circuits over $Σ$ can be thought of as string diagrams in the free monoidal category generated by $Σ$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the ca…
▽ More
It is well-known that combinatorial circuits are modeled mathematically by string diagrams in a monoidal category. Given a gate set $Σ$, the circuits over $Σ$ can be thought of as string diagrams in the free monoidal category generated by $Σ$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. Intuitively, this functor should be valued in parameterized families of unitary matices, though it is not immediately clear what this mean through a categorical lens. In this paper, we show that the parameterized semantics studied in prior work can be understood through enrichment and internal constructions. We determine sufficient conditions under which this construction yields a symmetric monoidal category, and suggest how these semantics could be extended to classical circuit analysis and parameterized equivalence checking.
△ Less
Submitted 21 January, 2025;
originally announced January 2025.
-
A Sound and Complete Equational Theory for 3-Qubit Toffoli-Hadamard Circuits
Authors:
Matthew Amy,
Neil J. Ross,
Scott Wesley
Abstract:
We give a sound and complete equational theory for 3-qubit quantum circuits over the Toffoli-Hadamard gate set { X, CX, CCX, H }. That is, we introduce a collection of true equations among Toffoli-Hadamard circuits on three qubits that is sufficient to derive any other true equation between such circuits. To obtain this equational theory, we first consider circuits over the Toffoli-K gate set { X,…
▽ More
We give a sound and complete equational theory for 3-qubit quantum circuits over the Toffoli-Hadamard gate set { X, CX, CCX, H }. That is, we introduce a collection of true equations among Toffoli-Hadamard circuits on three qubits that is sufficient to derive any other true equation between such circuits. To obtain this equational theory, we first consider circuits over the Toffoli-K gate set { X, CX, CCX, K }, where K = HxH. The Toffoli-Hadamard and Toffoli-K gate sets appear similar, but they are crucially different on exactly three qubits. Indeed, in this case, the former generates an infinite group of operators, while the latter generates the finite group of automorphisms of the well-known E8 lattice. We take advantage of this fact, and of the theory of automorphism groups of lattices, to obtain a sound and complete collection of equations for Toffoli-K circuits. We then extend this equational theory to one for Toffoli-Hadamard circuits by leveraging prior work of Li et al. on Toffoli-Hadamard operators.
△ Less
Submitted 12 August, 2024; v1 submitted 15 July, 2024;
originally announced July 2024.
-
LinguaQuanta: Towards a Quantum Transpiler Between OpenQASM and Quipper (Extended)
Authors:
Scott Wesley
Abstract:
As quantum computing evolves, many important questions emerge, such as how best to represent quantum programs, and how to promote interoperability between quantum program analysis tools. These questions arise naturally in the design of quantum transpilers, which translate between quantum programming languages. In this paper, we take a step towards answering these questions by identifying challenge…
▽ More
As quantum computing evolves, many important questions emerge, such as how best to represent quantum programs, and how to promote interoperability between quantum program analysis tools. These questions arise naturally in the design of quantum transpilers, which translate between quantum programming languages. In this paper, we take a step towards answering these questions by identifying challenges and best practices in quantum transpiler design. We base these recommendations on our experience designing LinguaQuanta, a quantum transpiler between Quipper and OpenQASM. First, we provide categorical specifications for quantum transpilers, which aim to encapsulate the core principles of the UNIX philosophy. We then identify quantum circuit decompositions which we expect to be useful in quantum transpilation. With these foundations in place, we then discuss challenges faced during the implementation of LinguaQuanta, such as ancilla management and stability under round translation. To show that LinguaQuanta works in practice, a short tutorial is given for the example of quantum phase estimation. We conclude with recommendations for the future of LinguaQuanta, and for quantum software development tools more broadly.
△ Less
Submitted 15 May, 2024; v1 submitted 11 April, 2024;
originally announced April 2024.
