Program Verification, Debugging, and QC Simulation

(Chong, Reppy, Franklin, Martonosi, Brown, Schuster, Harrow, Farhi, Shor)

Because quantum systems have such a large state space, they cannot be simulated efficiently on classical computers. Nonetheless, verification, debugging, and simulation are a critical part of architectural design. We will develop tractable methods to model quantum systems and software.

Program Verification

We note that there are certain subclasses of algorithms that can be simulated on a classical computer. The first are small algorithms where the whole space can be stored classically. These algorithms are useful tests for automated gate compilation. For example, automated compilation of small quantum chemistry problems at Microsoft revealed errors in the circuits reported in the literature. The second are algorithms whose output can be efficiently simulated due to the simplified nature of the circuits. The classic example of this are Clifford circuits where classical simulations scale quadratically in the size of the quantum circuit. These models are ideal for testing the performance of quantum circuits in the presence of noise and provide an idea of what noise levels still allow for a quantum advantage. Recent work by Bravyi and Gosset has shown that a few non-Clifford gates can be added without destroying the ability to simulate the system. Again these circuits allow us to test if our automated tools are correctly synthesizing circuits by comparing simulated to ideal outputs

Validation and verification for quantum computing

Quantum computations can be affected by both hardware and software errors. These can be further divided into hardware imperfections and mischaracterizations and on the software side, the algorithm might rely on assumptions which are unmet or the process of translating theory into gate sequences may simply have introduced bugs. These errors may be difficult to characterize, such as correlated noise, and may interact, such as a software bug which exposes a state to more decoherence than necessary. As a result, effective methods for validating and verifying quantum computations will be crucial to the success of early quantum computers. Ensuring the correctness of quantum computers will be important, and will present new challenges, as we enter the era of “quantum supremacy,” when quantum computations are performed that cannot be simulated on any classical computer. This non-simulability may, ironically, be a barrier to actually verifying that quantum supremacy has been achieved. Nevertheless, we will aim to develop efficient methods to test quantum computations and certify their results. To understand the limits of verification, we will attempt to derive negative results based on complexity theory. For example, a plausible test of a quantum circuit is a log-likelihood test, and indeed this was recently proposed by the quantum computing group at Google. The only known methods for carrying this out require exponential time, and we have preliminary results with evidence suggesting that it is unlikely to be possible in polynomial time. We will explore the extent to which plausible assumptions from complexity theory can be used to more generally limit the verifiability of quantum computations.

Technology Models and Libraries

Tremendous strides have been made in quantum computing hardware since the first quantum logic gate was demonstrated at NIST Boulder in 1995, work that was recognized with a Nobel prize awarded to David Wineland in 2012. Among the candidate physical platforms for QC, trapped ions and superconductors have shown substantial progress towards scaling to multi-qubit operations in the last five years, especially in industry and through the IARPA MQCO program. The EPiQC team includes leading experimental groups working on these two major platforms, where (1) a clear technical path towards scaling to a 1000 qubit level design exists, (2) a full set of universal quantum gates has been demonstrated, (3) qubit preparation and measurement can be performed with very high fidelity, and (4) the potential exists for implementing multi-qubit logical gates at the physical level, which provides promising opportunities for development of algorithms which leverage unique hardware capabilities.