Technical Perspective: A Symbolic Approach to Verifying Quantum Systems

Exceptional added value may lie in connecting two complementary areas of computer science. This statement is particularly true when applying mature techniques developed in one area to solve complex problems that arise in a new area. The accompanying paper, “An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits” by Lengál et al., is a case in point. It applies techniques developed in logic, automata, and symbolic verification to analyze the correctness of quantum programs.

The current quest of quantum computing is achieving quantum supremacy—that is, to reach the point where we solve problems that are practically unsolvable using conventional computing. To that end, substantial recent progress has been made in implementing quantum hardware and developing programming languages for quantum computers. In many applications, system correctness is of critical importance. For instance, identifying a subtle bug in a quantum circuit used for quantum chemistry simulations could prevent incorrect predictions about molecular interactions, which is critical for drug discovery and material design.

Given the complexity of quantum systems and the correctness requirements, tools for analyzing and verifying quantum programs’ correctness are demanded. However, building verification tools for quantum programs is immensely challenging due to their probabilistic nature and the exponential size of the computational space. Furthermore, there is a fundamental difference in how conventional and quantum computers process information: Conventional computers use digital bits (0s and 1s), while quantum computers deploy quantum bits (qubits) to store quantum information in values between 0 and 1.

The accompanying paper addresses whether we can exploit the research community’s vast experience in conventional program verification to develop tools for handling quantum systems. Verification tools, in general, and for quantum systems in particular, would ideally have the following properties:

• Flexibility: Allows flexible specification of properties of interest

• Diagnostics: Provides precise bug diagnostics

• Automation: Operates automatically

• Scalability: Scales efficiently to verify useful programs

Symbolic verification is one of the most successful techniques that satisfy the above criteria for conventional programs. To date, we have lacked an extension to the quantum realm due to the latter’s unique mathematical structure and different operational principles. The core of this work is the innovative application of automata theory, a cornerstone of formal verification, to quantum circuit verification. It combines tree automata-based reasoning with symbolic representations tailored for quantum circuits, allowing automated verification at unprecedented scales. It goes back to the very basics of program verification by recalling the classical Hoare triples {P}C{Q}, where {P} and {Q} are sets of quantum states representing the pre-condition and the post-condition, and C is a quantum circuit. It uses symbolic verification to check the validity of the triple, ensuring that all executions of C from states in P result in states within Q.

Although this is the first attempt to use such techniques in the context of quantum computing, implementing the framework with a tool gives spectacular results. For instance, the tool manages to verify large circuits with up to 40 qubits and 141,527 gates or catch bugs injected into circuits with up to 320 qubits and 1,758 gates, while all exiting tools fail to handle such benchmarks.

The framework’s success is based on the groundbreaking observation that we can lift core concepts of classical verification, such as state-space exploration and symbolic reasoning, into the quantum setting. This extension allows the verification of quantum circuits, offering a path to applying well-established classical paradigms in a domain where formal guarantees are critical.

In addition to its early practical promise, the approach opens new research directions in automata theory, where quantum structures introduce novel mathematical challenges and opportunities. It establishes a connection between quantum program verification and automata, promoting new possibilities to exploit the richness of automata theory and automata-based verification in quantum computing. It is worth noting that the methodology is not just about catching mistakes but also about building trust in quantum computing systems as we move toward an era in which they might solve problems classical systems cannot.

In conclusion, the accompanying paper represents a rare confluence of disciplines, opening pathways for collaboration between automata theorists, quantum physicists, and software engineers. Looking ahead, this line of research opens up exciting opportunities. Could similar automata-based techniques be adapted to other aspects of quantum software engineering? Could this approach handle quantum programming languages’ more abstract and flexible constructs? The authors’ combination of deep theoretical insights and practical tool development sets the stage for significant advancements in the field. Their results are a milestone for quantum circuit verification and a beacon guiding future research toward reliable quantum computation.