A key challenge of quantum programming is uncomputation: the reversible deallocation of qubits. And while there has been much recent progress on automating uncomputation, state-of-the-art methods are insufficient for handling today’s expressive quantum programming languages. A core reason is that they operate on primitive quantum circuits, while quantum programs express computations beyond circuits, for instance, they can capture families of circuits defined recursively in terms of uncomputation and adjoints.
In this paper we introduce the first modular automatic approach to synthesize correct and efficient uncomputation for expressive quantum programs. Our method is based on two core technical contributions: (i) an intermediate representation (IR) that can capture expressive quantum programs and comes with support for uncomputation, and (ii) a modular uncomputation and adjoint synthesis algorithms over that IR.
We have built a complete end-to-end implementation of our method including an implementation of the IR and the synthesis algorithms as well as a translation from an expressive fragment of the Silq programming language to our IR and circuit generation from the IR. Our experimental evaluation demonstrates that we can handle programs beyond the capabilities of existing uncomputation approaches, while being competitive on the benchmarks they can handle. More broadly, we show that it is possible to benefit from the greater expressivity and safety offered by high-level quantum languages without sacrificing efficiency.
Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:20 | |||
11:00 20mTalk | Modular Synthesis of Efficient Quantum Uncomputation OOPSLA 2024 Hristo Venev INSAIT, Sofia University "St. Kliment Ohridski", Timon Gehr ETH Zurich, Dimitar Dimitrov INSAIT, Sofia University, Martin Vechev ETH Zurich DOI | ||
11:20 20mTalk | Quantum Probabilistic Model Checking for Time-Bounded Properties OOPSLA 2024 Seungmin Jeon KAIST, Kyeongmin Cho KAIST, Chan Gu Kang Korea University, Janggun Lee KAIST, Hakjoo Oh Korea University, Jeehoon Kang KAIST DOI | ||
11:40 20mTalk | Quarl: A Learning-Based Quantum Circuit Optimizer OOPSLA 2024 Zikun Li Carnegie Mellon University, Jinjun Peng Columbia University, Yixuan Mei Carnegie Mellon University, Sina Lin Microsoft, Yi Wu Tsinghua University, Oded Padon VMware Research, Zhihao Jia Carnegie Mellon University DOI | ||
12:00 20mTalk | Synthetiq: Fast and Versatile Quantum Circuit Synthesis OOPSLA 2024 Anouk Paradis ETH Zurich, Jasper Dekoninck ETH Zurich, Benjamin Bichsel ETH Zurich, Switzerland, Martin Vechev ETH Zurich DOI |