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）上的可执行程序。