Collaborative Research: FMitF: Track I: Synthesizing Verifiable Compiler toward Fault-Tolerant Quantum Computing

Quantum computing has seen substantial progress, yet its high hardware error rates hamper its utility. The emerging solution to the problem is the use of sophisticated error correction, which is challenging to implement correctly. This project tackles this challenge at the software level. The project's novelty lies in its development of a verifiable quantum compiler that integrates formal methods with quantum computing. The work involves the automatic synthesis of fault-tolerant quantum programs, ensuring the correctness of quantum programs even after errors occur. The project's impacts are enhancements to the technological capabilities of quantum computing and assurances that these systems can be practically implemented and maintained in real-world applications with high reliability and efficiency. Quantum computing, if realized at scale, offers the potential to transform a variety of high-impact applications, including drug development, materials discovery, traffic optimization, and much more. This project supports the foundation on which these applications will be built. Further, the project's broader impact contributions include integrating project results within the academic curriculum at the investigators' home institutions and broadening participation through mentorship of students from populations underrepresented in computing. Collaborations with industry leaders will also support the adoption of innovative, verified quantum compilers and the development of widely applicable, empirically validated open-source technologies. The technical approach is multifaceted, aiming to advance Fault-Tolerant Quantum Computing by automating the generation of fault-tolerant quantum programs and ensuring their accuracy through rigorous verification. The team leverages complementary expertise in quantum computing and formal methods to address three critical tasks: (1) optimizing the translation of quantum algorithms into fault-tolerant implementations; (2) creating verifiable error detection tailored for quantum environments; and (3) developing decoders that deliver timely feedback to quantum hardware. 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.