Automated Theorem Proving for Quantum Circuit Verification using SAT Solvers

Jincheng Zhang

Published Sep 5, 2026• 0 citations

Abstract

The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.

DOI: 10.5281/zenodo.22339924

Related papers

Automated Theorem Proving for Quantum Circuit Verification using Abstract Interpretation

Jincheng Zhang

Quantum circuit verification is a critical yet notoriously challenging task in quantum computing. Full simulation of quantum circuits scales exponentially with the number of qubits and circuit depth, rendering it impractical for even moderately sized circuits. This paper proposes a novel approach to automated theorem proving for quantum circuit verification leveraging abstract interpretation. Our core idea is to approximate the behavior of quantum circuits using abstract interpretations, significantly reducing the computational complexity of the verification process. We outline a framework where abstract domains are constructed to represent the key properties of quantum circuits, such as qubit state fidelities and gate operations. The framework then employs logical reasoning and inference rules based on these abstract representations to automatically determine the correctness of a circuit against a given specification. We demonstrate the feasibility of this approach and discuss its potential to dramatically improve the efficiency and scalability of quantum circuit verification. The key benefit lies in shifting the verification burden from exact simulation to a more tractable abstract analysis.

Sep 1, 20260 citations

Formal Verification of Quantum Circuit Optimization Algorithms

Jincheng Zhang

Quantum circuit optimization is crucial for realizing the full potential of quantum computing. However, the inherent complexity of quantum circuits and the potential for errors introduce significant challenges in ensuring the correctness and efficiency of optimization algorithms. This paper proposes a novel approach to formally verify quantum circuit optimization algorithms. We translate these algorithms into formal specification languages and leverage model checking and theorem proving techniques to rigorously demonstrate that the algorithms meet their intended objectives – primarily minimizing circuit complexity – without introducing unintended side effects. The core contribution lies in applying formal verification methodologies to this largely unexplored area, offering a path towards building trust and confidence in quantum optimization strategies. The presented framework provides a systematic method for ensuring the reliability of quantum circuits, a critical step towards practical quantum computation. The verification process relies on defining the desired behavior as a set of logical properties and then employing automated tools to check whether the optimized circuit satisfies these properties. This approach addresses the fundamental need for rigorous assurance in quantum systems, moving beyond empirical validation and towards mathematically proven correctness.

Sep 5, 20260 citations

Boolean satisfiability verification by quantum annealing

Maria Maltseva, Александр Сергеевич Румянцев, Mariya Maltseva +1 more

The Boolean satisfiability problem (SAT) is widely applied in modern tasks of microelectronics design automation. An important application of such a task is the design of logic circuits with specified characteristics from a given set of logic gates. To solve an SAT problem, both standard solvers and modern optimization tools can be used, including a relatively new hardware tool for solving the quantum annealing problem. The solution of this problem can be performed on a quantum annealing system by constructing a socalled Boolean network according to special rules and selecting an appropriate objective function. The article discusses the practical application of quantum annealing to the construction of short logic circuits by solving an SAT problem based on the methods proposed in the literature, and also analyzes the practical aspects of applying such methods to the construction of quantum circuits.

Proceedings of the Karelian Research Centre of the Russian Academy of SciencesJun 23, 20231 citation

Temporal Logic-Based Formal Verification of Quantum Circuits

Jincheng Zhang

This paper presents a novel approach to verifying the correctness of quantum circuits using temporal logic. Traditional verification methods often rely on gate-level simulation, which can be computationally expensive and insufficient for complex quantum algorithms. This work addresses this limitation by formally modeling quantum circuits as temporal logic systems. We leverage the expressive power of temporal logic to capture the desired behavior of quantum algorithms, including their evolution over time and the effects of quantum phenomena like superposition and entanglement. The core of our method involves mapping the circuit's operations onto temporal logic specifications and utilizing automated theorem proving and model checking techniques, tailored to the probabilistic nature of quantum systems. We demonstrate that this approach provides a more rigorous and scalable verification framework compared to existing methods, offering a pathway to ensuring the reliability of quantum computations. The key contributions of this work are the formalization of quantum circuits with temporal logic, the adaptation of theorem proving and model checking techniques for quantum systems, and the potential for significantly improving the trustworthiness of quantum algorithms.

Aug 28, 20260 citations

qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking

Abhoy Kole, Mohammed Elkacem Djeridane, Lennart Weingarten +2 more

The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential runtime in several instances. In this work, we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover’s algorithm. The Exclusive-Sum-of-Product (ESOP)-based generation of the Conjunctive Normal Form (CNF) equivalent clauses demands less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover’s iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open source Qiskit platform and IBM quantum computer.

arXiv:2409.03917ACM Journal on Emerging Technologies in Computing SystemsApr 10, 20251 citation

A Review of Formal Methods in Quantum Circuit Verification

Arun Govindankutty

Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.

QeiosJan 8, 20260 citations