Eager: from theory to practice of quantum circuit decidability

The National Science Foundation Division of Information and Intelligent Systems awarded Kansas State University $400,000 on January 1, 2027, under the Computer and Information Science and Engineering program (CFDA 47.070) to develop a framework that automatically analyzes code to identify errors in quantum circuit translation and compilation.

The project, titled "From Theory to Practice of Quantum Circuit Decidability," integrates weighted model counting with a theory propagator that detects Pauli-transfer inconsistencies and commutativity constraints during conflict-driven search to provide better understanding of error propagation across multiple compilation stages: high-level code translation into gate-level circuits, gate count and depth optimization, circuit routing onto quantum hardware, and problem-space embedding into error-correcting codes. The work organizes into four thrusts: formal theory specification and mathematical property assessment; development of a custom satisfiability modulo theories user-propagator within the conflict-driven clause learning loop to generate dynamic conflict explanations and commutativity lemmas; integration of this propagator with a weighted model counting pipeline; and comprehensive benchmarking to validate reductions in decision branches and execution runtime. The recipient will make the entire toolchain and benchmarks fully open source.

Performance occurs in Manhattan, Kansas, with performance period from January 1, 2027, through December 31, 2028. The assistance type is Project Grant.

Abstract

Quantum computers are extremely powerful devices capable of solving certain problems much faster than traditional computers. However, programming these advanced systems is challenging, and converting code into instructions that the quantum hardware can interpret often introduces unwanted errors. This project will develop a framework that will automatically analyze code to identify these errors, ensuring that programs run correctly on quantum computer hardware. The intellectual merit of this work lies in the central idea that integrating weighted model counting with a theory propagator that detects pauli-transfer inconsistencies and commutativity constraints during conflict-driven search may provide a better understanding of error propagation during: high-level code translation into gate-level circuits; optimizing the gate count and depth; routing the circuit onto actual quantum hardware; and embedding the problem space into an error-correcting code. The project will integrate dynamic weighted pauli-basis reasoning directly into a constraint solver loop to efficiently verify quantum circuits. The project is organized into four specific thrusts. Thrust one develops a formal theory specification and assesses mathematical properties, such as convexity and theory combination compatibility. Thrust two creates a custom satisfiability modulo theories user-propagator within the conflict-driven clause learning loop to generate dynamic conflict explanations and commutativity lemmas. Thrust three incorporates this propagator with a weighted model counting pipeline. Thrust four conducts comprehensive benchmarking to validate reductions in decision branches and execution runtime. The project will have significant broader impacts by making the entire toolchain and benchmarks fully open source, thereby accelerating scientific discovery in this important field. Detecting errors in code translation will ensure the correctness of quantum programs, saving time and costs in the development and deployment of advanced quantum computer systems. The research findings will be integrated into kansas state university graduate courses for students with limited backgrounds in quantum computing. Educational outreach will include interactive quantum computing demonstrations for high school students at engineering open houses and technical presentations at major quantum computer and information science and engineering conferences to support workforce development. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the foundation's intellectual merit and broader impacts review criteria.- subawards are not planned for this award.