01576nas a2200181 4500008004100000022001400041245006300055210006100118260001400179300001600193490000600209520107500215100001701290700001701307700001801324700001501342856003701357 2024 eng d a2475-142100aA Case for Synthesis of Recursive Quantum Unitary Programs0 aCase for Synthesis of Recursive Quantum Unitary Programs c12/5/2023 a1759–17880 v83 a

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.

1 aDeng, Haowei1 aTao, Runzhou1 aPeng, Yuxiang1 aWu, Xiaodi uhttps://arxiv.org/abs/2311.1150302177nas a2200181 4500008004100000022001400041245009400055210006900149260001500218300001600233490000600249520163700255100001801892700001701910700001601927700001501943856003701958 2024 eng d a2475-142100aSimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation0 aSimuQ A Framework for Programming Quantum Hamiltonian Simulation c11/19/2023 a2425–24550 v83 a

Quantum Hamiltonian simulation, which simulates the evolution of quantum systems and probes quantum phenomena, is one of the most promising applications of quantum computing. Recent experimental results suggest that Hamiltonian-oriented analog quantum simulation would be advantageous over circuit-oriented digital quantum simulation in the Noisy Intermediate-Scale Quantum (NISQ) machine era. However, programming analog quantum simulators is much more challenging due to the lack of a unified interface between hardware and software. In this paper, we design and implement SimuQ, the first framework for quantum Hamiltonian simulation that supports Hamiltonian programming and pulse-level compilation to heterogeneous analog quantum simulators. Specifically, in SimuQ, front-end users specify the target quantum system with Hamiltonian Modeling Language, and the Hamiltonian-level programmability of analog quantum simulators is specified through a new abstraction called the abstract analog instruction set (AAIS) and programmed in AAIS Specification Language by hardware providers. Through a solver-based compilation, SimuQ generates executable pulse schedules for real devices to simulate the evolution of desired quantum systems, which is demonstrated on superconducting (IBM), neutral-atom (QuEra), and trapped-ion (IonQ) quantum devices. Moreover, we demonstrate the advantages of exposing the Hamiltonian-level programmability of devices with native operations or interaction-based gates and establish a small benchmark of quantum simulation to evaluate SimuQ's compiler with the above analog quantum simulators.

1 aPeng, Yuxiang1 aYoung, Jacob1 aLiu, Pengyu1 aWu, Xiaodi uhttps://arxiv.org/abs/2303.0277501923nas a2200253 4500008004100000020002200041245008700063210006900150260004800219520105800267100002001325700001901345700002301364700001501387700001601402700002401418700002001442700002201462700001201484700001501496700002201511700002201533856011401555 2023 eng d a978-3-031-38554-400aFixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium0 aFixing and Mechanizing the Security Proof of FiatShamir with Abo aChambSpringer Nature Switzerlandc8/9/20233 a

We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by the authors, and there seems to be no simple patch for it. We provide new, fixed proofs for the affected CMA-to-NMA reduction, both for the ROM and the QROM, and we perform a concrete security analysis for the case of Dilithium to show that the claimed security level is still valid after addressing the gap. Furthermore, we offer a fully mechanized ROM proof for the CMA-security of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.

1 aBarbosa, Manuel1 aBarthe, Gilles1 aDoczkal, Christian1 aDon, Jelle1 aFehr, Serge1 aGrégoire, Benjamin1 aHuang, Yu-Hsuan1 aHülsing, Andreas1 aLee, Yi1 aWu, Xiaodi1 aHandschuh, Helena1 aLysyanskaya, Anna uhttps://www.quics.umd.edu/publications/fixing-and-mechanizing-security-proof-fiat-shamir-aborts-and-dilithium01903nas a2200193 4500008004100000245006000041210006000101260001400161520128300175653004301458653002701501653002901528653003401557653003101591100001501622700002001637700001501657856003701672 2022 eng d00aDifferentiable Quantum Programming with Unbounded Loops0 aDifferentiable Quantum Programming with Unbounded Loops c11/8/20223 a

The emergence of variational quantum applications has led to the development of automatic differentiation techniques in quantum computing. Recently, Zhu et al. (PLDI 2020) have formulated differentiable quantum programming with bounded loops, providing a framework for scalable gradient calculation by quantum means for training quantum variational applications. However, promising parameterized quantum applications, e.g., quantum walk and unitary implementation, cannot be trained in the existing framework due to the natural involvement of unbounded loops. To fill in the gap, we provide the first differentiable quantum programming framework with unbounded loops, including a newly designed differentiation rule, code transformation, and their correctness proof. Technically, we introduce a randomized estimator for derivatives to deal with the infinite sum in the differentiation of unbounded loops, whose applicability in classical and probabilistic programming is also discussed. We implement our framework with Python and Q#, and demonstrate a reasonable sample efficiency. Through extensive case studies, we showcase an exciting application of our framework in automatically identifying close-to-optimal parameters for several parameterized quantum applications.

10aFOS: Computer and information sciences10aFOS: Physical sciences10aMachine Learning (cs.LG)10aProgramming Languages (cs.PL)10aQuantum Physics (quant-ph)1 aFang, Wang1 aYing, Mingsheng1 aWu, Xiaodi uhttps://arxiv.org/abs/2211.0450701921nas a2200205 4500008004100000245009400041210006900135260001500204520125300219653004301472653002701515653003401542653003101576100001301607700001701620700001201637700001401649700001501663856003701678 2022 eng d00aQuantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification0 aQuantum Natural Proof A New Perspective of Hybrid QuantumClassic c11/11/20223 a

Many quantum programs are assured by formal verification, but such verification is usually laborious and time-consuming. This paper proposes quantum natural proof (QNP), an automated proof system for verifying hybrid quantum-classical algorithms. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, provide sound but incomplete procedures, and capture common reasoning tactics in program verification. The core of QNP is a type-guided quantum proof system, named Qafny, which views quantum operations as some classical array operations that can be modeled as proof rules in a classical separation logic framework, suitable for automated reasoning. We proved the soundness and completeness of the Qafny proof system as well as the soundness of the proof system compilation from Qafny to Dafny. By using the QNP implementation in Dafny, automated verification can be efficiently perform for many hybrid quantum-classical algorithms, including GHZ, Shor's, Grover's, and quantum walk algorithms, which saves a great amount of human efforts. In addition, quantum programs written in Qafny can be compiled to quantum circuits so that every verified quantum program can be run on a quantum machine.

10aFOS: Computer and information sciences10aFOS: Physical sciences10aProgramming Languages (cs.PL)10aQuantum Physics (quant-ph)1 aLi, Liyi1 aZhu, Mingwei1 aLee, Yi1 aChang, Le1 aWu, Xiaodi uhttps://arxiv.org/abs/2211.06411