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 ten quantum unitary programs including quantum adder circuits, quantum eigenvalue inversion circuits and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.

翻译：量子程序因涉及反直觉的量子知识而难以编码与验证，因此能够减轻底层量子细节带来的繁琐与错误的自动化工具极具价值。本文首次开展针对递归定义不同输入规模酉电路族的量子酉程序合成研究——此类程序在现有量子编程语言中被广泛使用。具体而言，我们提出首个量子程序合成框架QSynth，包含新型归纳量子编程语言及其规约、用于推理的可靠逻辑体系，以及将推理过程编码为SMT实例的方法。通过利用现有SMT求解器，QSynth成功合成了包括量子加法器电路、量子本征值求逆电路和量子傅里叶变换在内的十个量子酉程序，这些程序可直接转换为Q#、IBM Qiskit和AWS Braket等主流量子平台的可执行程序。