← All insights

A circuit optimizer you can trust

Aria Language →aria · runtime · lean4 · optimizer

Aria bundles its runtime in the same repository (the omega-* crates), so what you read about here ships with the language at github.com/Anzaetek/aria-quantum-language-oss-public.

Three passes, run until nothing changes

The optimizer in omega-core does three things, in a loop, until the gate count stops moving:

  1. Remove what cancels. Two self-inverse gates in a row on the same qubit (H·H, X·X, CX·CX) are dropped, along with identity gates and zero-angle rotations.
  2. Merge rotations. Adjacent rotations around the same axis on the same qubit become one rotation with the summed angle.
  3. Commute to create more of both. Single-qubit gates move through multi-qubit gates where the algebra allows, which exposes new cancellations and merges for the next round.

That is deliberately small. It captures most of what a heavyweight optimizer gives you, and every rule is simple enough to check.

Checked, then proved

Each pass carries unit tests on the circuits it rewrites, and every example circuit is checked numerically against an independent oracle end to end, so a rewrite that changed a result would fail the suite. The self-inverse identities behind the cancellation pass (H, X, Y, Z and CNOT) are proved in the Lean 4 tree that ships with Aria (proofs/lean4/QuantumProofs/Gates.lean), alongside the gate matrices and circuit semantics the other passes rely on.

The rest of the runtime

The same crates give you what the optimizer sits next to:

  • Gradients. Exact adjoint differentiation for one-pass parameter gradients, and CMA-ES when a loss is noisy or not differentiable.
  • Dynamic circuits. Mid-circuit measurement, conditional gates and reset on every backend; the reset semantics are formalized too (ResetModel.lean).
  • Observables. Build Pauli sums with operator arithmetic and evaluate several at once from one simulation.

Why it matters

Speed is table stakes; many simulators are fast. What you need from a runtime is that rewriting a circuit does not quietly change what it computes. That is what the tests and the proofs are for.