Showing 1–22 of 22 results for author: Amy, M

Linear and non-linear relational analyses for Quantum Program Optimization

Authors: Matthew Amy, Joseph Lunderville

Abstract: The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a l… ▽ More The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program. We show that the phase folding optimization can be re-cast as an \emph{affine relation analysis}, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum \emph{programs} with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for \emph{non-linear} relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations -- such as Clifford+$T$ -- we show that the \emph{sum-over-paths} technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand. △ Less

Submitted 30 October, 2024; originally announced October 2024.

Comments: 30 pages, 13 figures, comments welcome!

Journal ref: Proc. ACM Program. Lang. 9, POPL, Article 37 (January 2025), 33 pages

Polynomial-Time Classical Simulation of Hidden Shift Circuits via Confluent Rewriting of Symbolic Sums

Authors: Matthew Amy, Lucas Shigeru Stinchcombe

Abstract: Implementations of Roetteler's shifted bent function algorithm have in recent years been used to test and benchmark both classical simulation algorithms and quantum hardware. These circuits have many favorable properties, including a tunable amount of non-Clifford resources and a deterministic output, and moreover do not belong to any class of quantum circuits which is known to be efficiently simu… ▽ More Implementations of Roetteler's shifted bent function algorithm have in recent years been used to test and benchmark both classical simulation algorithms and quantum hardware. These circuits have many favorable properties, including a tunable amount of non-Clifford resources and a deterministic output, and moreover do not belong to any class of quantum circuits which is known to be efficiently simulable. We show that this family of circuits can in fact be simulated in polynomial time via symbolic path integrals. We do so by endowing symbolic sums with a confluent rewriting system and show that this rewriting system suffices to reduce the circuit's path integral to the hidden shift in polynomial-time. We hence resolve an open conjecture about the efficient simulability of this class of circuits. △ Less

Submitted 5 August, 2024; originally announced August 2024.

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.

Comments: In Proceedings QPL 2024, arXiv:2408.05113

Journal ref: EPTCS 406, 2024, pp. 1-43

Exact Synthesis of Multiqubit Clifford-Cyclotomic Circuits

Authors: Matthew Amy, Andrew N. Glaudell, Shaun Kelso, William Maxwell, Samuel S. Mendelson, Neil J. Ross

Abstract: Let $n\geq 8$ be divisible by 4. The Clifford-cyclotomic gate set $\mathcal{G}_n$ is the universal gate set obtained by extending the Clifford gates with the $z$-rotation $T_n = \mathrm{diag}(1,ζ_n)$, where $ζ_n$ is a primitive $n$-th root of unity. In this note, we show that, when $n$ is a power of 2, a multiqubit unitary matrix $U$ can be exactly represented by a circuit over $\mathcal{G}_n$ if… ▽ More Let $n\geq 8$ be divisible by 4. The Clifford-cyclotomic gate set $\mathcal{G}_n$ is the universal gate set obtained by extending the Clifford gates with the $z$-rotation $T_n = \mathrm{diag}(1,ζ_n)$, where $ζ_n$ is a primitive $n$-th root of unity. In this note, we show that, when $n$ is a power of 2, a multiqubit unitary matrix $U$ can be exactly represented by a circuit over $\mathcal{G}_n$ if and only if the entries of $U$ belong to the ring $\mathbb{Z}[1/2,ζ_n]$. We moreover show that $\log(n)-2$ ancillas are always sufficient to construct a circuit for $U$. Our results generalize prior work to an infinite family of gate sets and show that the limitations that apply to single-qubit unitaries, for which the correspondence between Clifford-cyclotomic operators and matrices over $\mathbb{Z}[1/2,ζ_n]$ fails for all but finitely many values of $n$, can be overcome through the use of ancillas. △ Less

Submitted 12 April, 2024; v1 submitted 13 November, 2023; originally announced November 2023.

Optimising quantum circuits is generally hard

Authors: John van de Wetering, Matt Amy

Abstract: In order for quantum computations to be done as efficiently as possible it is important to optimise the number of gates used in the underlying quantum circuits. In this paper we find that many gate optimisation problems for approximately universal quantum circuits are NP-hard. In particular, we show that optimising the T-count or T-depth in Clifford+T circuits, which are important metrics for the… ▽ More In order for quantum computations to be done as efficiently as possible it is important to optimise the number of gates used in the underlying quantum circuits. In this paper we find that many gate optimisation problems for approximately universal quantum circuits are NP-hard. In particular, we show that optimising the T-count or T-depth in Clifford+T circuits, which are important metrics for the computational cost of executing fault-tolerant quantum computations, is NP-hard by reducing the problem to Boolean satisfiability. With a similar argument we show that optimising the number of CNOT gates or Hadamard gates in a Clifford+T circuit is also NP-hard. Again varying the same argument we also establish the hardness of optimising the number of Toffoli gates in a reversible classical circuit. We find an upper bound to the problems of T-count and Toffoli-count of $\text{NP}^{\text{NQP}}$. Finally, we also show that for any non-Clifford gate $G$ it is NP-hard to optimise the $G$-count over the Clifford+$G$ gate set, where we only have to match the target unitary within some small distance in the operator norm. △ Less

Submitted 12 August, 2024; v1 submitted 12 September, 2023; originally announced October 2023.

Comments: v3: Changed title from "Optimising T-count is NP-hard", rewrote paper with additional results about other optimisation problems

Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes

Authors: Matthew Amy

Abstract: Vilmart recently gave a complete equational theory for the balanced sum-over-paths over Toffoli-Hadamard circuits, and by extension Clifford+Rz(2pi/2^k) circuits. Their theory is based on the phase-free ZH-calculus which crucially omits the average rule of the full ZH-calculus, dis-allowing the local summation of amplitudes. Here we study the question of completeness in unbalanced path sums which… ▽ More Vilmart recently gave a complete equational theory for the balanced sum-over-paths over Toffoli-Hadamard circuits, and by extension Clifford+Rz(2pi/2^k) circuits. Their theory is based on the phase-free ZH-calculus which crucially omits the average rule of the full ZH-calculus, dis-allowing the local summation of amplitudes. Here we study the question of completeness in unbalanced path sums which naturally support local summation. We give a concrete syntax for the unbalanced sum-over-paths and show that, together with symbolic multilinear algebra and the interference rule, various formulations of the average and ortho rules of the ZH-calculus are sufficient to give complete equational theories over arbitrary rings and fields. △ Less

Submitted 31 August, 2023; v1 submitted 28 June, 2023; originally announced June 2023.

Comments: In Proceedings QPL 2023, arXiv:2308.15489

Journal ref: EPTCS 384, 2023, pp. 127-141

Improved Synthesis of Toffoli-Hadamard Circuits

Authors: Matthew Amy, Andrew N. Glaudell, Sarah Meng Li, Neil J. Ross

Abstract: The matrices that can be exactly represented by a circuit over the Toffoli-Hadamard gate set are the orthogonal matrices of the form $M/ \sqrt{2}{}^k$, where $M$ is an integer matrix and $k$ is a nonnegative integer. The exact synthesis problem for this gate set is the problem of constructing a circuit for a given such matrix. Existing methods produce circuits consisting of $O(2^n \log(n)k)$ gates… ▽ More The matrices that can be exactly represented by a circuit over the Toffoli-Hadamard gate set are the orthogonal matrices of the form $M/ \sqrt{2}{}^k$, where $M$ is an integer matrix and $k$ is a nonnegative integer. The exact synthesis problem for this gate set is the problem of constructing a circuit for a given such matrix. Existing methods produce circuits consisting of $O(2^n \log(n)k)$ gates, where $n$ is the dimension of the matrix. In this paper, we provide two improved synthesis methods. First, we show that a technique introduced by Kliuchnikov in 2013 for Clifford+$T$ circuits can be straightforwardly adapted to Toffoli-Hadamard circuits, reducing the complexity of the synthesized circuit from $O(2^n \log(n)k)$ to $O(n^2 \log(n)k)$. Then, we present an alternative synthesis method of similarly improved cost, but whose application is restricted to circuits on no more than three qubits. Our results also apply to orthogonal matrices over the dyadic fractions, which correspond to circuits using the 2-qubit gate $H\otimes H$, rather than the usual single-qubit Hadamard gate $H$. △ Less

Submitted 18 May, 2023; originally announced May 2023.

Catalytic Embeddings of Quantum Circuits

Authors: M. Amy, M. Crawford, A. N. Glaudell, M. L. Macasieb, S. S. Mendelson, N. J. Ross

Abstract: If a set $\mathbb{G}$ of quantum gates is countable, then the operators that can be exactly represented by a circuit over $\mathbb{G}$ form a strict subset of the collection of all unitary operators. When $\mathbb{G}$ is universal, one circumvents this limitation by resorting to repeated gate approximations: every occurrence of a gate which cannot be exactly represented over $\mathbb{G}$ is replac… ▽ More If a set $\mathbb{G}$ of quantum gates is countable, then the operators that can be exactly represented by a circuit over $\mathbb{G}$ form a strict subset of the collection of all unitary operators. When $\mathbb{G}$ is universal, one circumvents this limitation by resorting to repeated gate approximations: every occurrence of a gate which cannot be exactly represented over $\mathbb{G}$ is replaced by an approximating circuit. Here, we introduce catalytic embeddings, which provide an alternative to repeated gate approximations. With catalytic embeddings, approximations are relegated to the preparation of a fixed number of reusable resource states called catalysts. Because the catalysts only need to be prepared once, when catalytic embeddings exist they always produce shorter circuits, in the limit of increasing gate count and target precision. In the present paper, we lay the foundations of the theory of catalytic embeddings and we establish several of their structural properties. In addition, we provide methods to design catalytic embeddings, showing that their construction can be reduced to that of a single fixed matrix when the gates involved have entries in well-behaved rings of algebraic numbers. Finally, we showcase some concrete examples and applications. Notably, we show that catalytic embeddings generalize a technique previously used to implement the Quantum Fourier Transform over the Clifford+$T$ gate set with $O(n)$ gate approximations. △ Less

Submitted 12 May, 2023; originally announced May 2023.

Symbolic Synthesis of Clifford Circuits and Beyond

Authors: Matthew Amy, Owen Bennett-Gibbs, Neil J. Ross

Abstract: Path sums are a convenient symbolic formalism for quantum operations with applications to the simulation, optimization, and verification of quantum protocols. Unlike quantum circuits, path sums are not limited to unitary operations, but can express arbitrary linear ones. Two problems, therefore, naturally arise in the study of path sums: the unitarity problem and the extraction problem. The former… ▽ More Path sums are a convenient symbolic formalism for quantum operations with applications to the simulation, optimization, and verification of quantum protocols. Unlike quantum circuits, path sums are not limited to unitary operations, but can express arbitrary linear ones. Two problems, therefore, naturally arise in the study of path sums: the unitarity problem and the extraction problem. The former is the problem of deciding whether a given path sum represents a unitary operator. The latter is the problem of constructing a quantum circuit, given a path sum promised to represent a unitary operator. In this paper, we show that the unitarity problem is co-NP-hard in general, but that it is in P when restricted to Clifford path sums. We then provide an algorithm to synthesize a Clifford circuit from a unitary Clifford path sum. The circuits produced by our extraction algorithm are of the form C1-H-C2, where C1 and C2 are Hadamard-free circuits and H is a layer of Hadamard gates. We also provide a heuristic generalization of our extraction algorithm to arbitrary path sums. While this algorithm is not guaranteed to succeed, it often succeeds and typically produces natural looking circuits. Alongside applications to the optimization and decompilation of quantum circuits, we demonstrate the capability of our algorithm by synthesizing the standard quantum Fourier transform directly from a path sum. △ Less

Submitted 15 November, 2023; v1 submitted 29 April, 2022; originally announced April 2022.

Comments: In Proceedings QPL 2022, arXiv:2311.08375

Journal ref: EPTCS 394, 2023, pp. 343-362

The phase/state duality in reversible circuit design

Authors: Matthew Amy, Neil J. Ross

Abstract: The reversible implementation of classical functions accounts for the bulk of most known quantum algorithms. As a result, a number of reversible circuit constructions over the Clifford+$T$ gate set have been developed in recent years which use both the state and phase spaces, or $X$ and $Z$ bases, to reduce circuit costs beyond what is possible at the strictly classical level. We study and general… ▽ More The reversible implementation of classical functions accounts for the bulk of most known quantum algorithms. As a result, a number of reversible circuit constructions over the Clifford+$T$ gate set have been developed in recent years which use both the state and phase spaces, or $X$ and $Z$ bases, to reduce circuit costs beyond what is possible at the strictly classical level. We study and generalize two particular classes of these constructions: relative phase circuits, including Giles and Selinger's multiply-controlled $iX$ gates and Maslov's $4$ qubit Toffoli gate, and measurement-assisted circuits, including Jones' Toffoli gate and Gidney's temporary logical-AND. In doing so, we introduce general methods for implementing classical functions up to phase and for measurement-assisted termination of temporary values. We then apply these techniques to find novel $T$-count efficient constructions of some classical functions in space-constrained regimes, notably multiply-controlled Toffoli gates and temporary products. △ Less

Submitted 5 November, 2021; v1 submitted 27 May, 2021; originally announced May 2021.

Comments: 16 pages, comments welcome

Journal ref: Phys. Rev. A 104, 052602 (2021)

staq -- A full-stack quantum processing toolkit

Authors: Matthew Amy, Vlad Gheorghiu

Abstract: We describe 'staq', a full-stack quantum processing toolkit written in standard C++. 'staq' is a quantum compiler toolkit, comprising of tools that range from quantum optimizers and translators to physical mappers for quantum devices with restricted connectives. The design of 'staq' is inspired from the UNIX philosophy of "less is more", i.e. 'staq' achieves complex functionality via combining (pi… ▽ More We describe 'staq', a full-stack quantum processing toolkit written in standard C++. 'staq' is a quantum compiler toolkit, comprising of tools that range from quantum optimizers and translators to physical mappers for quantum devices with restricted connectives. The design of 'staq' is inspired from the UNIX philosophy of "less is more", i.e. 'staq' achieves complex functionality via combining (piping) small tools, each of which performs a single task using the most advanced current state-of-the-art methods. We also provide a set of illustrative benchmarks. △ Less

Submitted 5 August, 2020; v1 submitted 12 December, 2019; originally announced December 2019.

Comments: Replaced with the published version, comments are welcome

Journal ref: Quantum Science and Technology, Focus on Quantum Software, 5, 034016 (2020)

Number-Theoretic Characterizations of Some Restricted Clifford+T Circuits

Authors: Matthew Amy, Andrew N. Glaudell, Neil J. Ross

Abstract: Kliuchnikov, Maslov, and Mosca proved in 2012 that a $2\times 2$ unitary matrix $V$ can be exactly represented by a single-qubit Clifford+$T$ circuit if and only if the entries of $V$ belong to the ring $\mathbb{Z}[1/\sqrt{2},i]$. Later that year, Giles and Selinger showed that the same restriction applies to matrices that can be exactly represented by a multi-qubit Clifford+$T$ circuit. These num… ▽ More Kliuchnikov, Maslov, and Mosca proved in 2012 that a $2\times 2$ unitary matrix $V$ can be exactly represented by a single-qubit Clifford+$T$ circuit if and only if the entries of $V$ belong to the ring $\mathbb{Z}[1/\sqrt{2},i]$. Later that year, Giles and Selinger showed that the same restriction applies to matrices that can be exactly represented by a multi-qubit Clifford+$T$ circuit. These number-theoretic characterizations shed new light upon the structure of Clifford+$T$ circuits and led to remarkable developments in the field of quantum compiling. In the present paper, we provide number-theoretic characterizations for certain restricted Clifford+$T$ circuits by considering unitary matrices over subrings of $\mathbb{Z}[1/\sqrt{2},i]$. We focus on the subrings $\mathbb{Z}[1/2]$, $\mathbb{Z}[1/\sqrt{2}]$, $\mathbb{Z}[1/i\sqrt{2}]$, and $\mathbb{Z}[1/2,i]$, and we prove that unitary matrices with entries in these rings correspond to circuits over well-known universal gate sets. In each case, the desired gate set is obtained by extending the set of classical reversible gates $\{X, CX, CCX\}$ with an analogue of the Hadamard gate and an optional phase gate. △ Less

Submitted 3 April, 2020; v1 submitted 16 August, 2019; originally announced August 2019.

Journal ref: Quantum 4, 252 (2020)

Sized Types for low-level Quantum Metaprogramming

Authors: Matthew Amy

Abstract: One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, an ability which is of particular importance in the context of quantum computing as algorithms frequently use arithmetic over non-standard word l… ▽ More One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, an ability which is of particular importance in the context of quantum computing as algorithms frequently use arithmetic over non-standard word lengths. In this work, we introduce metaQASM, a typed extension of the openQASM language supporting the metaprogramming of circuit families. Our language and type system, built around a lightweight implementation of sized types, supports subtyping over register sizes and is moreover type-safe. In particular, we prove that our system is strongly normalizing, and as such any well-typed metaQASM program can be statically unrolled into a finite circuit. △ Less

Submitted 7 August, 2019; originally announced August 2019.

Comments: Presented at Reversible Computation 2019. Final authenticated publication is available online at https://doi.org/10.1007/978-3-030-21500-2_6

Journal ref: Thomsen M., Soeken M. (eds) Reversible Computation. RC 2019. Lecture Notes in Computer Science, vol 11497. Springer, Cham

Towards Large-scale Functional Verification of Universal Quantum Circuits

Authors: Matthew Amy

Abstract: We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy… ▽ More We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy with respect to either a specification or reference circuit is enabled by a novel rewrite system for exponential sums with free variables. Our algorithm is further shown to give a polynomial-time decision procedure for checking the equivalence of Clifford group circuits. We evaluate our methods by performing automated verification of optimized Clifford+T circuits with up to 100 qubits and thousands of T gates, as well as the functional verification of quantum algorithms using hundreds of qubits. Our experiments culminate in the automated verification of the Hidden Shift algorithm for a class of Boolean functions in a fraction of the time it has taken recent algorithms to simulate. △ Less

Submitted 29 January, 2019; v1 submitted 17 May, 2018; originally announced May 2018.

Comments: In Proceedings QPL 2018, arXiv:1901.09476

Journal ref: EPTCS 287, 2019, pp. 1-21

Strawberry Fields: A Software Platform for Photonic Quantum Computing

Authors: Nathan Killoran, Josh Izaac, Nicolás Quesada, Ville Bergholm, Matthew Amy, Christian Weedbrook

Abstract: We introduce Strawberry Fields, an open-source quantum programming architecture for light-based quantum computers, and detail its key features. Built in Python, Strawberry Fields is a full-stack library for design, simulation, optimization, and quantum machine learning of continuous-variable circuits. The platform consists of three main components: (i) an API for quantum programming based on an ea… ▽ More We introduce Strawberry Fields, an open-source quantum programming architecture for light-based quantum computers, and detail its key features. Built in Python, Strawberry Fields is a full-stack library for design, simulation, optimization, and quantum machine learning of continuous-variable circuits. The platform consists of three main components: (i) an API for quantum programming based on an easy-to-use language named Blackbird; (ii) a suite of three virtual quantum computer backends, built in NumPy and TensorFlow, each targeting specialized uses; and (iii) an engine which can compile Blackbird programs on various backends, including the three built-in simulators, and -- in the near future -- photonic quantum information processors. The library also contains examples of several paradigmatic algorithms, including teleportation, (Gaussian) boson sampling, instantaneous quantum polynomial, Hamiltonian simulation, and variational quantum circuit optimization. △ Less

Submitted 4 March, 2019; v1 submitted 9 April, 2018; originally announced April 2018.

Comments: Try the Strawberry Fields Interactive website, located at http://strawberryfields.ai . Source code available at https://github.com/XanaduAI/strawberryfields. Accepted in Quantum

Journal ref: Quantum 3, 129 (2019)

On the CNOT-complexity of CNOT-PHASE circuits

Authors: Matthew Amy, Parsiad Azimzadeh, Michele Mosca

Abstract: We study the problem of CNOT-optimal quantum circuit synthesis over gate sets consisting of CNOT and Z-basis rotations of arbitrary angles. We show that the circuit-polynomial correspondence relates such circuits to Fourier expansions of pseudo-Boolean functions, and that for certain classes of functions this expansion uniquely determines the minimum CNOT cost of an implementation. As a corollary… ▽ More We study the problem of CNOT-optimal quantum circuit synthesis over gate sets consisting of CNOT and Z-basis rotations of arbitrary angles. We show that the circuit-polynomial correspondence relates such circuits to Fourier expansions of pseudo-Boolean functions, and that for certain classes of functions this expansion uniquely determines the minimum CNOT cost of an implementation. As a corollary we prove that CNOT minimization over CNOT and phase gates is at least as hard as synthesizing a CNOT-optimal circuit computing a set of parities of its inputs. We then show that this problem is NP-complete for two restricted cases where all CNOT gates are required to have the same target, and where the circuit inputs are encoded in a larger state space. The latter case has applications to CNOT optimization over more general Clifford+T circuits. We further present an efficient heuristic algorithm for synthesizing circuits over CNOT and Z-basis rotations with small CNOT cost. Our experiments show a 23% reduction of CNOT gates on average across a suite of Clifford+T benchmark circuits, with a maximum reduction of 43%. △ Less

Submitted 13 August, 2018; v1 submitted 5 December, 2017; originally announced December 2017.

Comments: 21 pages, 5 figures, 1 table. Version 2 formally verifies the correctness of the benchmark optimizations, 4 out of 39 are left unverified due to size, Quantum Science and Technology, 2018

Journal ref: Quantum Science and Technology 4(1), 2018

A Finite Presentation of CNOT-Dihedral Operators

Authors: Matthew Amy, Jianxin Chen, Neil J. Ross

Abstract: We give a finite presentation by generators and relations of the unitary operators expressible over the {CNOT, T, X} gate set, also known as CNOT-dihedral operators. To this end, we introduce a notion of normal form for CNOT-dihedral circuits and prove that every CNOT-dihedral operator admits a unique normal form. Moreover, we show that in the presence of certain structural rules only finitely man… ▽ More We give a finite presentation by generators and relations of the unitary operators expressible over the {CNOT, T, X} gate set, also known as CNOT-dihedral operators. To this end, we introduce a notion of normal form for CNOT-dihedral circuits and prove that every CNOT-dihedral operator admits a unique normal form. Moreover, we show that in the presence of certain structural rules only finitely many circuit identities are required to reduce an arbitrary CNOT-dihedral circuit to its normal form. By appropriately restricting our relations, we obtain a finite presentation of unitary operators expressible over the {CNOT, T} gate set as a corollary. △ Less

Submitted 28 April, 2019; v1 submitted 31 December, 2016; originally announced January 2017.

Comments: In Proceedings QPL 2017, arXiv:1802.09737

Journal ref: EPTCS 266, 2018, pp. 84-97

Estimating the cost of generic quantum pre-image attacks on SHA-2 and SHA-3

Authors: Matthew Amy, Olivia Di Matteo, Vlad Gheorghiu, Michele Mosca, Alex Parent, John Schanck

Abstract: We investigate the cost of Grover's quantum search algorithm when used in the context of pre-image attacks on the SHA-2 and SHA-3 families of hash functions. Our cost model assumes that the attack is run on a surface code based fault-tolerant quantum computer. Our estimates rely on a time-area metric that costs the number of logical qubits times the depth of the circuit in units of surface code cy… ▽ More We investigate the cost of Grover's quantum search algorithm when used in the context of pre-image attacks on the SHA-2 and SHA-3 families of hash functions. Our cost model assumes that the attack is run on a surface code based fault-tolerant quantum computer. Our estimates rely on a time-area metric that costs the number of logical qubits times the depth of the circuit in units of surface code cycles. As a surface code cycle involves a significant classical processing stage, our cost estimates allow for crude, but direct, comparisons of classical and quantum algorithms. We exhibit a circuit for a pre-image attack on SHA-256 that is approximately $2^{153.8}$ surface code cycles deep and requires approximately $2^{12.6}$ logical qubits. This yields an overall cost of $2^{166.4}$ logical-qubit-cycles. Likewise we exhibit a SHA3-256 circuit that is approximately $2^{146.5}$ surface code cycles deep and requires approximately $2^{20}$ logical qubits for a total cost of, again, $2^{166.5}$ logical-qubit-cycles. Both attacks require on the order of $2^{128}$ queries in a quantum black-box model, hence our results suggest that executing these attacks may be as much as $275$ billion times more expensive than one would expect from the simple query analysis. △ Less

Submitted 30 November, 2016; v1 submitted 30 March, 2016; originally announced March 2016.

Comments: Same as the published version to appear in the Selected Areas of Cryptography (SAC) 2016. Comments are welcome!

Verified compilation of space-efficient reversible circuits

Authors: Matthew Amy, Martin Roetteler, Krysta Svore

Abstract: The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent on… ▽ More The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent on verifying the correctness of the results, an issue of particular importance in quantum computing. There, compilation allows not only mapping to hardware, but also the estimation of resources required to implement a given quantum algorithm, a process that is crucial for identifying which algorithms will outperform their classical counterparts. We present a reversible circuit compiler called ReVerC, which has been formally verified in F* and compiles circuits that operate correctly with respect to the input program. Our compiler compiles the Revs language to combinational reversible circuits with as few ancillary bits as possible, and provably cleans temporary values. △ Less

Submitted 20 April, 2018; v1 submitted 4 March, 2016; originally announced March 2016.

Comments: Proceedings version. New section on eager cleanup, general streamlining

Journal ref: Proceedings of the 29th International Conference on Computer Aided Verification, pp. 3-21, 2017

T-count optimization and Reed-Muller codes

Authors: Matthew Amy, Michele Mosca

Abstract: In this paper, we study the close relationship between Reed-Muller codes and single-qubit phase gates from the perspective of $T$-count optimization. We prove that minimizing the number of $T$ gates in an $n$-qubit quantum circuit over CNOT and $T$, together with the Clifford group powers of $T$, corresponds to finding a minimum distance decoding of a length $2^n-1$ binary vector in the order… ▽ More In this paper, we study the close relationship between Reed-Muller codes and single-qubit phase gates from the perspective of $T$-count optimization. We prove that minimizing the number of $T$ gates in an $n$-qubit quantum circuit over CNOT and $T$, together with the Clifford group powers of $T$, corresponds to finding a minimum distance decoding of a length $2^n-1$ binary vector in the order $n-4$ punctured Reed-Muller code. Moreover, we show that the problems are polynomially equivalent in the length of the code. As a consequence, we derive an algorithm for the optimization of $T$-count in quantum circuits based on Reed-Muller decoders, along with a new upper bound of $O(n^2)$ on the number of $T$ gates required to implement an $n$-qubit unitary over CNOT and $T$ gates. We further generalize this result to show that minimizing small angle rotations corresponds to decoding lower order binary Reed-Muller codes. In particular, we show that minimizing the number of $R_Z(2π/d)$ gates for any integer $d$ is equivalent to minimum distance decoding in $\mathcal{RM}(n - k - 1, n)^*$, where $k$ is the highest power of $2$ dividing $d$. △ Less

Submitted 13 August, 2018; v1 submitted 27 January, 2016; originally announced January 2016.

Comments: 19 pages. Version 2 gives a substantially different presentation of the results, as well as a generalization to rotation angles of any finite order

Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning

Authors: Matthew Amy, Dmitri Maslov, Michele Mosca

Abstract: Most work in quantum circuit optimization has been performed in isolation from the results of quantum fault-tolerance. Here we present a polynomial-time algorithm for optimizing quantum circuits that takes the actual implementation of fault-tolerant logical gates into consideration. Our algorithm re-synthesizes quantum circuits composed of Clifford group and T gates, the latter being typically the… ▽ More Most work in quantum circuit optimization has been performed in isolation from the results of quantum fault-tolerance. Here we present a polynomial-time algorithm for optimizing quantum circuits that takes the actual implementation of fault-tolerant logical gates into consideration. Our algorithm re-synthesizes quantum circuits composed of Clifford group and T gates, the latter being typically the most costly gate in fault-tolerant models, e.g., those based on the Steane or surface codes, with the purpose of minimizing both T-count and T-depth. A major feature of the algorithm is the ability to re-synthesize circuits with additional ancillae to reduce T-depth at effectively no cost. The tested benchmarks show up to 65.7% reduction in T-count and up to 87.6% reduction in T-depth without ancillae, or 99.7% reduction in T-depth using ancillae. △ Less

Submitted 13 December, 2013; v1 submitted 8 March, 2013; originally announced March 2013.

Comments: Version 2 contains substantial improvements and extensions to the previous version. We describe a new, more robust algorithm and achieve significantly improved experimental results

Journal ref: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 33(10): 1476-1489, 2014

A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits

Authors: Matthew Amy, Dmitri Maslov, Michele Mosca, Martin Roetteler

Abstract: We present an algorithm for computing depth-optimal decompositions of logical operations, leveraging a meet-in-the-middle technique to provide a significant speed-up over simple brute force algorithms. As an illustration of our method we implemented this algorithm and found factorizations of the commonly used quantum logical operations into elementary gates in the Clifford+T set. In particular, we… ▽ More We present an algorithm for computing depth-optimal decompositions of logical operations, leveraging a meet-in-the-middle technique to provide a significant speed-up over simple brute force algorithms. As an illustration of our method we implemented this algorithm and found factorizations of the commonly used quantum logical operations into elementary gates in the Clifford+T set. In particular, we report a decomposition of the Toffoli gate over the set of Clifford and T gates. Our decomposition achieves a total T-depth of 3, thereby providing a 40% reduction over the previously best known decomposition for the Toffoli gate. Due to the size of the search space the algorithm is only practical for small parameters, such as the number of qubits, and the number of gates in an optimal implementation. △ Less

Submitted 25 January, 2013; v1 submitted 4 June, 2012; originally announced June 2012.

Comments: 23 pages, 15 figures, 1 table; To appear in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

Journal ref: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 32(6): 818-830, 2013