A Verified Optimizer for Quantum Circuits

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks
12/4/2019
cs.PLcs.ETcs.LO

Official code: inQWIRE/SQIR (107 stars, MIT, last commit 2026-04-02).

Abstract

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.

View on arXivView PDF

Code Implementations(1)

inQWIRE/SQIROfficial100%
MIT

A Small Quantum Intermediate Representation

10726Dune, MakefileDec 20, 20186 months agoMIT
compiler-constructioncoqquantum-computing

Similar Papers

Evaluating Mutation Techniques in Genetic Algorithm-Based Quantum Circuit Synthesis

87% match2025

Particle Swarm Optimization for Quantum Circuit Synthesis: Performance Analysis and Insights

85% match2025

ScaffCC: Scalable Compilation and Analysis of Quantum Programs

85% match2015

Quantum Optimization Algorithms

85% match2025

Strawberry Fields: A Software Platform for Photonic Quantum Computing

84% match1 repo8552018

QSpark: Towards Reliable Qiskit Code Generation

84% match2025

Cite this paper

@article{hietala2019verified,
  title  = {A Verified Optimizer for Quantum Circuits},
  author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks},
  year   = {2019},
  eprint = {1912.02250},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1912.02250}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1912.02250.svg)](https://codeofpaper.com/paper/1912.02250)

Discussion