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.
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.
Kliuchnikov, Maslov, and Mosca proved in 2012 that a
2
×
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
Z
1
/
...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
Z
1
/
2
,
i
. We focus on the subrings
Z
1
/
2
,
Z
1
/
2
,
Z
1
/
i
2
, and
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
,
C
X
,
C
C
X
}
with an analogue of the Hadamard gate and an optional phase gate.
T-Count Optimization and Reed-Muller Codes Amy, Matthew; Mosca, Michele
IEEE transactions on information theory,
2019-Aug., 2019-8-00, Volume:
65, Issue:
8
Journal Article
Peer reviewed
Open access
In this paper, we study the close relationship between Reed-Muller codes and single-qubit phase gates from the perspective of <inline-formula> <tex-math notation="LaTeX">T ...</tex-math></inline-formula>-count optimization. We prove that minimizing the number of <inline-formula> <tex-math notation="LaTeX">T </tex-math></inline-formula> gates in an <inline-formula> <tex-math notation="LaTeX">n </tex-math></inline-formula>-qubit quantum circuit over CNOT and <inline-formula> <tex-math notation="LaTeX">T </tex-math></inline-formula>, together with the Clifford group powers of <inline-formula> <tex-math notation="LaTeX">T </tex-math></inline-formula>, corresponds to finding a minimum distance decoding of a length <inline-formula> <tex-math notation="LaTeX">2^{n}-1 </tex-math></inline-formula> binary vector in the order <inline-formula> <tex-math notation="LaTeX">n-4 </tex-math></inline-formula> 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 <inline-formula> <tex-math notation="LaTeX">T </tex-math></inline-formula>-count in quantum circuits based on Reed-Muller decoders, along with a new upper bound of <inline-formula> <tex-math notation="LaTeX">O(n^{2}) </tex-math></inline-formula> on the number of <inline-formula> <tex-math notation="LaTeX">T </tex-math></inline-formula> gates required to implement an <inline-formula> <tex-math notation="LaTeX">n </tex-math></inline-formula>-qubit unitary over CNOT and <inline-formula> <tex-math notation="LaTeX">T </tex-math></inline-formula> 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 <inline-formula> <tex-math notation="LaTeX">R_{Z}(2\pi /m) </tex-math></inline-formula> gates for any integer <inline-formula> <tex-math notation="LaTeX">m </tex-math></inline-formula> is equivalent to minimum distance decoding in <inline-formula> <tex-math notation="LaTeX">\mathcal {RM}(n-k-1, n)^{*} </tex-math></inline-formula>, where <inline-formula> <tex-math notation="LaTeX">k </tex-math></inline-formula> is the highest power of 2 dividing <inline-formula> <tex-math notation="LaTeX">m </tex-math></inline-formula>.
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.
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 resynthesizes 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 resynthesize circuits with ancillae at effectively no additional cost, allowing space-time trade-offs to be easily explored. 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.
PDF
