Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation
Abstract
Fault-tolerant quantum compilers implement gates through Pauli-product measurements and classical feedback. Verifying such a compiler requires reasoning about the quantum state and the recorded outcomes together: a correction reads an outcome, a gate's internal outcomes must be hidden from its caller, and an application's outcomes must survive optimization. We introduce QPPM, a language for Pauli-product measurement programs, with a weakest-precondition semantics over store-indexed matrix assertions, following quantum Hoare logic with classical variables. Every program terminates, so the Hoare logic is a syntactic presentation of weakest preconditions whose soundness and relative completeness are immediate. Its value is that component specifications compose. All results are mechanized in Lean. We verify lowering of Clifford+T circuits to QPPM with private outcomes and supplied magic states, and an optimizer that eliminates measurements, fuses and reorders rotations, and schedules logical rounds while preserving every outcome that subsequent code can read. A compositional approximation relation bounds the effect of synthesis error on specifications and on output trace distance, and a certificate-checked pipeline selects, among synthesized circuits that meet the user's error limit, the one with the lowest certified depth bound. On QASMBench, verified fusion and scheduling reduce logical measurement depth by a median of 17.9\%, and complete source-to-QPPM allowances are certified for all 35 valid selected small-suite inputs.
Related
- A Platform-aware Compilation Framework for Fault-tolerant Quantum Computation
- Modular optical fault-tolerant quantum computation via an interface between verified resources and online logical operations
- C-Phase-Aware Compilation for Efficient Fault-Tolerant Quantum Execution
- FT-Weave: Real-Time Compilation Framework for Reconfigurable Fault-Tolerant Quantum Architectures
- CUDA-Q Logical: Retargetable Compilation for Fault-Tolerant Quantum Computing
BibTeX
@misc{ye2026verified,
title = {{Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation}},
author = {John Zhuoyang Ye and Jens Palsberg},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.31694},
eprint = {2610.31694},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.31694},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation
AU - John Zhuoyang Ye
AU - Jens Palsberg
PY - 2026
DA - 2026/10/20
PB - arXiv
DO - 10.48550/arxiv.2610.31694
UR - https://arxiv.org/abs/2610.31694
AB - Fault-tolerant quantum compilers implement gates through Pauli-product measurements and classical feedback. Verifying such a compiler requires reasoning about the quantum state and the recorded outcomes together: a correction reads an outcome, a gate's internal outcomes must be hidden from its caller, and an application's outcomes must survive optimization. We introduce QPPM, a language for Pauli-product measurement programs, with a weakest-precondition semantics over store-indexed matrix assertions, following quantum Hoare logic with classical variables. Every program terminates, so the Hoare logic is a syntactic presentation of weakest preconditions whose soundness and relative completeness are immediate. Its value is that component specifications compose. All results are mechanized in Lean. We verify lowering of Clifford+T circuits to QPPM with private outcomes and supplied magic states, and an optimizer that eliminates measurements, fuses and reorders rotations, and schedules logical rounds while preserving every outcome that subsequent code can read. A compositional approximation relation bounds the effect of synthesis error on specifications and on output trace distance, and a certificate-checked pipeline selects, among synthesized circuits that meet the user's error limit, the one with the lowest certified depth bound. On QASMBench, verified fusion and scheduling reduce logical measurement depth by a median of 17.9\%, and complete source-to-QPPM allowances are certified for all 35 valid selected small-suite inputs.
ER -