Bounds for Quantum Circuits using Logic-Based Analysis
Benedikt Fauseweh, Ben Hermann, Falk Howar
TL;DR
This paper introduces logic-based methods, including SMT solvers and over-approximation, to verify and bound properties of quantum circuits, demonstrated through Hamming weight preservation examples.
Contribution
It proposes novel compositional and linear over-approximation strategies for quantum circuit verification using SMT solvers.
Findings
Successful application to Hamming weight preservation
Demonstrated scalability of verification methods
Provided bounds for quantum circuit properties
Abstract
We explore ideas for scaling verification methods for quantum circuits using SMT (Satisfiability Modulo Theories) solvers. We propose two primary strategies: (1) decomposing proof obligations via compositional verification and (2) leveraging linear over-approximation techniques for gate effects. We present two examples and demonstrate the application of these ideas to proof Hamming weight preservation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Computing Algorithms and Architecture · Low-power high-performance VLSI design · Quantum Information and Cryptography