Efficiently Verifying Quantum Programs with Few T Gates

doi:10.1007/978-3-032-15700-3_3

Return

Efficiently Verifying Quantum Programs with Few T Gates

2026-01-01

PRE

Cho, Youngchan *

Rand, Robert

DOI：10.1007/978-3-032-15700-3_3

Original

Original request for help

Save

Abstract

En 中文

We mechanize a lightweight quantum logic in the Rocq proof assistant to verify Clifford+T quantum programs, particularly those with low T counts. Our tool is lightweight and automation-centric: Hoare triple validation composes simple rules, reduces all obligations to syntactic well-formedness side-conditions, and efficiently discharges those conditions. We demonstrate our tool using several case studies: a standard low-T Toffoli decomposition, graph-state generators, and the 7-qubit Steane encoder. A small empirical study on graph-state families shows near-linear growth in the number of Clifford gates and a slightly super-quadratic trend in the number of qubits, consistent with implementation overheads from list-based tensor representations, while repeated T gates on a single qubit exhibit an exponential blow-up due to additive branching. The results indicate that a rule-driven, syntax-directed approach suffices to verify low-T quantum circuits while keeping the trusted core and user-facing proofs simple.

Keywords:

hoare logic

quantum computing

proof assistants

Rocq