A Case for Synthesis of Recursive Quantum Unitary Programs
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 \emph{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.
Thu 18 JanDisplayed time zone: London change
09:00 - 10:20 | Synthesis 2POPL at Kelvin Lecture Chair(s): Michael Hicks Amazon Web Services and the University of Maryland | ||
09:00 20mTalk | Semantic Code Refactoring for Abstract Data Types POPL Shankara Pailoor University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin | ||
09:20 20mTalk | API-driven Program Synthesis for Testing Static Typing Implementations POPL Thodoris Sotiropoulos ETH Zurich, Stefanos Chaliasos Imperial College London, Zhendong Su ETH Zurich | ||
09:40 20mTalk | Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs POPL Kevin Batz RWTH Aachen University, Tom Biskup RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University | ||
10:00 20mTalk | A Case for Synthesis of Recursive Quantum Unitary Programs POPL Haowei Deng University of Maryland at College Park, Runzhou Tao Columbia University, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland |