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
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

Directions

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

- physical

Table of Content

Quartz

verify that our new n+1n+1 representation is actually correct by SMT solver

- physical

verify that our new $n+1$ representation is actually correct by SMT solver