P7: Scaling Verification of Digital Quantum Simulation

Members: Prof. Dr. Benedikt Fauseweh (TU Dortmund), Prof. Dr. Ben Hermann (TU Dortmund), Prof. Dr. Falk Howar (TU Dortmund), Yanick Kind (TU Dortmund)

Quantum computing holds the potential to revolutionize science and technology, with applications ranging from cryptography to material science. One promising application is Digital Quantum Simulation (DQS), which enables the modeling of quantum systems on digital quantum devices. However, as quantum circuits grow in qubit count, depth, and complexity, analyzing their properties becomes increasingly challenging. Verification techniques must address the scalability problem, which arises from the exponential growth of the state space, complex interactions among qubits, and the extensive depth of modern circuits.

This project aims to develop a **scalable, automated, and compositional framework** for the **verification of digital quantum simulations**.

By leveraging techniques from formal verification, program analysis, and domain-specific optimizations, the project will address three major challenges:

1. the encoding explosion of global gate effects, which limits scalability to large numbers of qubits;
2. the automation of finding intermediate properties for decomposing verification tasks, enabling analysis of circuits with complex gate fabrics; and
3. decomposing verification over time to handle deep circuits with many iterations.

The research will be organized into four work packages: 

1. Use Cases and Benchmarks: Identify representative quantum circuits and properties to evaluate the verification framework.
2. Verification Techniques: Develop novel methods, including assume-guarantee reasoning, weakest precondition transformers, and property-directed reachability, to verify large and complex quantum circuits.
3. Automation and Decomposition: Design and implement automated tools for discovering local properties, leveraging data-flow analysis and static analysis to decompose tasks effectively.
4. Integration and Demonstration: Combine these components into a unified framework, demonstrating scalability through comprehensive evaluation on benchmarks relevant to digital quantum simulations.

The field of digital quantum simulation will benefit broadly from this framework. The verification of symmetry preservation is crucial information in the simulation of quantum physics or quantum chemistry. Using these scalable methods will allow simulations to make educated decisions on symmetry preserving circuits and symmetry-breaking circuits. Furthermore, is the verification of quantum circuits with guaranteed properties very helpful in the programming of NISQ quantum hardware. By the end of the project, we aim to deliver a robust, scalable verification framework implemented in a prototypical tool. This tool will be validated on real-world use cases, providing empirical evidence of its effectiveness. The results of this project will advance the state of the art in quantum circuit verification and quantum software engineering.