Quartz

Quantum System: building automatic quantum compiler

Equivalent Circuit Classes (ECCs): a set of circuits that perform the same task

subsumed transformation: valid transformation
$(n,q)$ -complete EECs: biggest EEC of certain function that has at most $n$ gates and $q$ qubits

Subcircuit: a collection of gates in a circuits that are executed in close neighborehood of computation graph. (If I execute subcircuit in appropriate time, it will never go wrong.)

Parametric gates: gates that needs input to define and construct. For a circuit with $m$ parameters and $q$ qubits, the circuit is written as:

$[[C]]: \mathbb{R}^m \to \mathbb{C}^{2^q \times 2^q}$

Equivalence: $|\psi\rangle$ and $e^{i\beta}|\psi\rangle$ is equivalent up to a global phase. From an observational point of view, they are identical.

Circuit: $C^{(n, q)}$

fix gate set $G$
fixed parameter expression $\Sigma$

Representative Circuit: an arbitrary circuit that is one of the smallest in a EEC set in which the functionality is what we care about. // TODO: you should put definition of representation in front. and you didn't define "previous round" to have EECs instead of one EEC.

Circuit Transformation: a tuple $(C_T, C_R)$ is a target and a rewrite. An EEC with $x$ circuit has $x(x-1)$ many transformations.

Fingerprint: randomly fix parameter $p_0$ and two quantum state, the finger print of a circuit is the following.

$|\langle \psi_0 | [[C]](\vec{p_0})|\psi_1\rangle|$

Pipeline: transformation generation and transformation applier

Generation:

start from representation with $n$ gates
add one gate to representation, now with $n+1$ gates but with redundant (possibly different functionality, but we track them non-the-less)
eliminate redundant representation to get new $n+1$ representation
- keep only simple random equivalence test
- pruning unused qubits
- pruning permutation of parameters
- remove transform that share parts of common transform
- verify that our new $n+1$ representation is actually correct by SMT solver

Applier:

circuit pruning
circuit optimizer: apply local transformation to the whole circuit based on cost before qubit mapping based on queue of cost using TASO. It applies transformation to some "almost-best" cost circuit (not seen before).

Performance: generation takes 30 min. Reduction gate count around 40%.

// QUESTION: why verifier?

// QUESTION: section related to phrase factor is unclear to me. Why SMT prover cannot prove Quartz

Given the number of qubits, we can prove a bound on how many CNOT to use at maximum. However, this bound isn't very useful if you don't assume full connectivity between all qubits. You can use SWAP (which uses 3 CNOT gate), but will be 4x~9x longer. Also, since physically you can't make your unitrary transform accurate, we just might as well evaluate the optimized algorithm by distance close to original matrix.

Since CNOT and U3 can represent all unitrary, we can transform the space of all possible CNOT and U3 combination into a tree space. We can do A on a tree space with some fitted heuristic function generated by brute force search. Brute force search for three qubit QFT takes one hour, while A takes only seven minutes.

Directions

fault tolerance = application
physical level is not done
quartz: logical
mapping
physical

Question:

assumption on connectivity
assumption on logical gate set
assumption on actual gate set

Table of Content