一句话：提出首个量子酉程序合成框架 QSynth，借助 SMT 求解自动合成递归定义的量子酉电路。
量子程序因涉及非直觉的量子知识而难以编写与验证，亟需自动化工具缓解底层量子细节带来的繁琐与错误。本文开创性地研究递归定义一族不同输入规模酉电路的量子程序合成问题。作者提出 QSynth——首个量子程序合成框架，包含一种新的归纳量子编程语言、其规约、可靠推理逻辑，以及将推理过程编码为 SMT 实例的机制。借助现有 SMT 求解器，QSynth 成功合成 10 个量子酉程序，涵盖量子算术程序、量子特征值求逆、量子隐形传态与量子傅里叶变换等，且可转译为 Q#、IBM Qiskit 和 AWS Braket 等主流量子平台上的可执行程序。
Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we initiate the study of program synthesis for quantum unitary programs that recursively define a family of unitary circuits for different input sizes, which are widely used in existing quantum programming languages. Specifically, we present QSynth, the first quantum program synthesis framework, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes 10 quantum unitary programs including quantum arithmetic programs, quantum eigenvalue inversion, quantum teleportation and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.
@article{paperbot2574,
title = {A Case for Synthesis of Recursive Quantum Unitary Programs},
author = {Haowei Deng and Runzhou Tao and Yuxiang Peng and Xiaodi Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632901}
}