A Case for Synthesis of Recursive Quantum Unitary Programs

Abstract

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.

References in corpus (22)

• Quantum secret sharing
• Quantum algorithm for solving linear systems of equations
• Synthesis of Quantum Logic Circuits
• A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits
• Quantum measurements and the Abelian Stabilizer Problem
• An approximate Fourier transform useful in quantum factoring
• A new quantum ripple-carry addition circuit
• Improved classical simulation of quantum circuits dominated by Clifford gates
• Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning
• Synthesis of Quantum Circuits for Linear Nearest Neighbor Architectures
• Towards Large-scale Functional Verification of Universal Quantum Circuits
• A Verified Optimizer for Quantum Circuits
• On the CNOT-complexity of CNOT-PHASE circuits
• A Deductive Verification Framework for Circuit-building Quantum Programs
• T-count optimization and Reed-Muller codes
• A Quantum Observable for the Graph Isomorphism Problem
• Synthesizing Quantum-Circuit Optimizers
• symQV: Automated Symbolic Verification of Quantum Programs
• Semantics-Guided Synthesis
• Quantum circuits and low-degree polynomials over F_2
• Quantum Dialogue by Using the GHZ State
• QPanda: high-performance quantum computing framework for multiple application scenarios

Cited by in corpus (5)

• FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
• Reinforcement learning with learned gadgets to tackle hard quantum problems on real hardware
• Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs
• Towards a quantum synapse for quantum sensing
• Hybrid Path-Sums for Hybrid Quantum Programs