A Case for Synthesis of Recursive Quantum Unitary Programs
summary
QSynth synthesizes recursive unitary programs by combining an inductive quantum language with a fixed‑point rule, a hypothesis‑amplitude input/output specification, and an SMT encoding of a new verification logic. It produces ten benchmarks (quantum adder, eigenvalue inversion, Quantum Fourier Transform, etc.), transpiles to Q#, Qiskit and Braket, and claims constant synthesis time while prior circuit synthesizers QSync and QFast time out at size 6. Artifacts are available and evaluated. SMT encoding
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:45Quantum programming challenges
- 3:51Motivation for synthesis
- 6:19QSyns framework overview
- 8:28Quantum basics example
- 11:39Extending QSquare
- 13:48Verification with complex numbers
- 15:13Amplitude form for verification
- 17:20Evaluation vs tools
- 19:10Q&A
related talks
20mSynthetiq: Fast and Versatile Quantum Circuit Synthesis
45mInteractive Proofs for Synthesizing Quantum States and Unitaries
15mModular Component-Based Quantum Circuit Synthesis
01h 10mThe Rise & Collapse of a Quantum State
20mQuantum Register Machine: Efficient Implementation of Quantum Recursive Programs
22mHow to Synthesize Quantum-Circuit Optimizers
15mToward A Quantum Programming Language for Higher Level Formal Verification
24mSynthesizing Quantum-Circuit Optimizers