[Feature Request] Circuit verification via ISM

[gwwatkin]

Issue Description

We want a technique to verify large scale circuits. Verification by comparing the final state-vector is computationally very expensive. A better approach might be to compare the logical circuit and the compiled circuit to a standard form, that is particularly efficient to compare.

Proposed Solution

Convert both logical and patch computation circuit into an Initialization-Stabilizer-Measurement form (ISM). Check that the initial states are the same for both, check that the stabilizer parts are the same by simulation with CHP on a set that generates all stabilizer states, check that measurements occur in the same order.

Overview

Our input quantum program is reversible quantum program, a unitary U_0, applied to an initial state v_0. Remove all the T gates by turning them into teleported gates, and our program is U, u. Now the compiled version of this program is a sequence of merges and splits on a large input state v_0. These are pure stabilizer operations in the Pauli formalism forming a unitary V, with the addition of some ancillas turning the initial state v_0 to v.

We check that u and v match (qubit mapping problem) and that U=V by checking UV^=1 (by ^ I mean dagger) with some efficient multiplier for stabilizer unitaries (based on CHP?).

Matching input qubits

Need to check that u and v match:

• Check that logical qubits map to the same inputs for U and V. They should just be the first n quits of the state vector. This mapping should be preserved by compilation and in the worst case we can track if we permute something
• Ancilla states are the same. This is a little trickier because we have 2 kinds of ancillas: |+> and |m>, but as long as it's possible to permute the ancilla portions v to match u that should be fine. Will have to track this permutation in V as well.

Checking Unitaries

We want to show that U (stabilizer ops of the logical circuit) is the same as V (stabilizer ops of the compiled circuit). We do it by checking that U|s> = V|s> a set as states |s> that generates all stabilizer states. TODO explain why this is enough.

The generator for all stabilizer states

What are the states |s> for which we check U|s> = V|s>? One state stabilized by each of the following Pauli products

XII...I, IXI...I, IIX...I,  ...  , III...X
YII...I, IYI...I, IIY...I,  ...  , III...Y 
ZII...I, IZI...I, IIZ...I,  ...  , III...Z 

Checking the measurement sequence

Need to look into this more as it might be tricky especially when running things like Litinski's transform for commuting pi/4 rotations.

Computing U|s> and V|s>

For the input circuit U it might be advantageous to use the Clifford+T set as it's more likely to be closer to the form in which the input was specified in to begin with.
On this set we can use CHP to compute U|s>. CHP internally uses the Pauli Product form to express stabilizer states (CHP paper beginning of sec. III), so we are in good shape for using these strings of paulis directly as input.

For the compiled compilation part we want to look at either decomposing the multibody measurements in their computational meaning with CNOTs and Hadamards or simulating them directly since they are stabilizer operations

Additional References

Paler et al. on converting circuits to ICM
Aaronson's CHP
Very Fast Stabilizer Simulator (Stim)
Graph state based fast stabilizer simulation (another idea for stabilizer simulation)

[gwwatkin]

Posting here the first draft of the issue for reference:

Proposed Solution (First draft)

Use the Initialization-CNOT-Measurement (ICM) form. In this form, the computation is expressed as initialization of states (including magic states), a unitary consisting of just CNOTS, and single measurements in the Z and X bases.

Verification process

Comparing Unitaries

Our input quantum program is reversible quantum program, a unitary U_0, applied to an initial state v_0. Remove all the T gates by turning them into teleported gates, and our program is U, u. Now the compiled version of this program is a sequence of merges and splits on a large input state v_0. This sequence can be broken down into CNOT operations forming a unitary V, with the addition of some ancillas turning the initial state into v.

We check that u and v match (qubit mapping problem) and that U=V by checking UV^=1 (by ^ I mean dagger) with some efficient multiplier for stabilizer unitaries (based on CHP?).

If the above are met, then the final state of both program should be Uu=Vv giving us high confidence that compilation is correct.

Challenges

• Converting merges and splits of multi-body measurements on more than two patches might be tricky, we'd have to break down what is going on in the ancilla region. Solution: Treat the ancilla region as one qubit in the |+1> state and the interactions with patches as CNOTs and CNOTs with Hadamards
• I'm not 100% on how we map the ancilla qubits used to do the multibody measurements (not the ones used for teleported gates which should map 1-to-1) to the ancilla qubits generated by the ICM conversion of the logical circuit. Solution: This should not be a problem because all the unmapped ancillas should be |+>.
• Is it enough to check that VU^|0...0>=|0...0> with CHP to show that V=U? I would guess that (if that's the case) it would emerge from properties of stabilizers I can't think of. However, for any permutation P|0..0> = |0..0> Solution: VU^|psi>=|psi> for a stabilizer set as states. I should be able to find out what these states are by looking at sections I, II and III of Aaronson's CHP paper
• If I'm wrong of the above, we have to look at a custom way of computing VU^. Looks like implementations of algorithms for Gottesman-Knill/CHP focus on simulation and are not designed with an API to access their inner workings. We would need such an interface to efficiently check if two unitaries applied one after the other are the identity (VU^=1). Solution: Not a problem because of the above

Other notes

• A lot of extra steps are a lot room for additional errors, especially if some of these steps are not already provided by software packages
• It might take a while to implement many ad-hoc steps
• Can use opflow to covert from merges and splits to stabilizer ops, or even zx rules