Synthesizing Quantum-Circuit Optimizers
Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, Aws Albarghouthi
Abstract
Near-term quantum computers are expected to work in an environment where each operation is noisy, with no error correction. Therefore, quantum-circuit optimizers are applied to minimize the number of noisy operations. Today, physicists are constantly experimenting with novel devices and architectures. For every new physical substrate and for every modification of a quantum computer, we need to modify or rewrite major pieces of the optimizer to run successful experiments. In this paper, we present QUESO, an efficient approach for automatically synthesizing a quantum-circuit optimizer for a given quantum device. For instance, in 1.2 minutes, QUESO can synthesize an optimizer with high-probability correctness guarantees for IBM computers that significantly outperforms leading compilers, such as IBM's Qiskit and TKET, on the majority (85%) of the circuits in a diverse benchmark suite. A number of theoretical and algorithmic insights underlie QUESO: (1) An algebraic approach for representing rewrite rules and their semantics. This facilitates reasoning about complex symbolic rewrite rules that are beyond the scope of existing techniques. (2) A fast approach for probabilistically verifying equivalence of quantum circuits by reducing the problem to a special form of polynomial identity testing . (3) A novel probabilistic data structure, called a polynomial identity filter (PIF), for efficiently synthesizing rewrite rules. (4) A beam-search-based algorithm that efficiently applies the synthesized symbolic rewrite rules to optimize quantum circuits.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 430e9c7c-8cad-4c5e-aec4-ac230a0f5098Cited by top-tier papers13
- Quarl: A Learning-Based Quantum Circuit OptimizerZikun Li, Jinjun Peng, Yixuan Mei, Sina Lin et al.OOPSLA 2024 · 21 citations
- Equality Saturation Theory Exploration à la CarteAnjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey et al.OOPSLA 2023 · 11 citations
- The T-Complexity Costs of Error Correction for Control Flow in Quantum ComputationCharles Yuan, Michael CarbinPLDI 2024 · 10 citations
- A Case for Synthesis of Recursive Quantum Unitary ProgramsHaowei Deng, Runzhou Tao, Yuxiang Peng, Xiaodi WuPOPL 2024 · 10 citations
- Linear and Non-linear Relational Analyses for Quantum Program OptimizationMatthew Amy, Joseph LundervillePOPL 2025 · 9 citations
Builds on12
- Software Mitigation of Crosstalk on Noisy Intermediate-Scale Quantum ComputersPrakash Murali, David C. McKay, Margaret Martonosi, Ali Javadi-AbhariASPLOS 2020 · 253 citations
- egg: Fast and extensible equality saturationMax Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt et al.POPL 2021 · 170 citations
- A verified optimizer for Quantum circuitsKesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu et al.POPL 2021 · 111 citations
- Alive2: bounded translation validation for LLVMNuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu et al.PLDI 2021 · 109 citations
- PET: Optimizing Tensor Programs with Partially Equivalent Transformations and Automated CorrectionsHaojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma et al.OSDI 2021 · 77 citations
Related papers
- Synthesis of Compact and Expressive Quantum-Circuit OptimizationsWei Qiang, Ronghui GuOOPSLA 2026
- Quartz: superoptimization of Quantum circuitsMingkuan Xu, Zikun Li, Oded Padon, Sina Lin et al.PLDI 2022 · 57 citations
- Equality Saturation for Quantum Circuit OptimizationGanxiang Yang, Paige Raun, Runzhou Tao, Ronghui GuPLDI 2026
- Relational Verification for Cost-Aware Quantum Program OptimizationZiming Zhao, Tingting Li, Zhaoxuan Li, Jianwei YinAAAI 2026
- Optimizing Quantum Circuits, Fast and SlowAmanda Xu, Abtin Molavi, Swamit Tannu, Aws AlbarghouthiASPLOS 2025 · 8 citations
