A Verified Compiler for Quantum Simulation
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912605860265984 |
|---|---|
| author | Li, Liyi An, Fenfen Zahariev, Federico Chong, Zhi Xiang Sabry, Amr Gordon, Mark S. |
| author_facet | Li, Liyi An, Fenfen Zahariev, Federico Chong, Zhi Xiang Sabry, Amr Gordon, Mark S. |
| contents | Hamiltonian simulation is a central application of quantum computing, with significant potential in modeling physical systems and solving complex optimization problems. Existing compilers for such simulations typically focus on low-level representations based on Pauli operators, limiting programmability and offering no formal guarantees of correctness across the compilation pipeline. We introduce QBlue, a high-level, formally verified framework for compiling Hamiltonian simulations. QBlue is based on the formalism of second quantization, which provides a natural and expressive way to describe quantum particle systems using creation and annihilation operators. To ensure safety and correctness, QBlue includes a type system that tracks particle types and enforces Hermitian structure. The framework supports compilation to both digital and analog quantum circuits and captures multiple layers of semantics, from static constraints to dynamic evolution. All components of QBlue, including its language design, type system, and compilation correctness, are fully mechanized in the Rocq proof framework, making it the first end-to-end verified compiler for second-quantized Hamiltonian simulation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_18583 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Verified Compiler for Quantum Simulation Li, Liyi An, Fenfen Zahariev, Federico Chong, Zhi Xiang Sabry, Amr Gordon, Mark S. Programming Languages Quantum Physics Hamiltonian simulation is a central application of quantum computing, with significant potential in modeling physical systems and solving complex optimization problems. Existing compilers for such simulations typically focus on low-level representations based on Pauli operators, limiting programmability and offering no formal guarantees of correctness across the compilation pipeline. We introduce QBlue, a high-level, formally verified framework for compiling Hamiltonian simulations. QBlue is based on the formalism of second quantization, which provides a natural and expressive way to describe quantum particle systems using creation and annihilation operators. To ensure safety and correctness, QBlue includes a type system that tracks particle types and enforces Hermitian structure. The framework supports compilation to both digital and analog quantum circuits and captures multiple layers of semantics, from static constraints to dynamic evolution. All components of QBlue, including its language design, type system, and compilation correctness, are fully mechanized in the Rocq proof framework, making it the first end-to-end verified compiler for second-quantized Hamiltonian simulation. |
| title | A Verified Compiler for Quantum Simulation |
| topic | Programming Languages Quantum Physics |
| url | https://arxiv.org/abs/2509.18583 |