Automated Verification of Hamiltonian Simulation by Quantum Signal Processing
Abstract
We present, to the best of our knowledge, the first fully automated verification framework for QSP-based Hamiltonian simulation. Our framework exploits the structure of the simulation algorithm: Hamiltonians are given as weighted sums of Pauli strings, embedded into larger unitaries through block encodings, and transformed into time-evolution operators by quantum signal processing (QSP). Using a symbolic Pauli-sum semantics for ancilla-indexed circuit blocks, our verifier proves that the distinguished all-zero ancilla block is proportional to the target Hamiltonian and infers the subnormalization factor automatically. It then verifies the QSP layer by extracting the implemented polynomial transformation and certifying its approximation error. This structure-aware abstraction is essential for scalability. Composing our verified block encoding and QSP wrapper yields an estimated macro-expanded size of about 1.52 million gates. The verifier certifies the block encoding once and checks the QSP layer through its abstract interface, without expanding the oracle calls. Our implementation verifies block encodings of structured Pauli-sum Hamiltonians with up to 256 system qubits and verifies QSP Hamiltonian-simulation instances by extracting their implemented polynomials and checking the resulting approximation bounds. These results show that fully automated verification can handle common Hamiltonian-simulation circuits at substantial scale when it exploits their algorithmic structure.
Related
- Observable-targeted variational quantum simulation of Hamiltonian dynamics
- Efficient Quantum Simulation of Linearized Vlasov--Poisson Dynamics Using Trotter and THRIFT Hamiltonian Simulation Methods
- Quantum Simulation of Two-Dimensional Free Dirac Hamiltonian in Multimode Circuit QED
- QBX: A Compiler for 2-local Qubit Hamiltonian Simulation on Quantum Chiplets
- Spin Hamiltonian for Quantum Simulation of Minimally Truncated 3+1D SU(2) Lattice Gauge Theory and Testing Eigenstate Thermalization
BibTeX
@misc{lai2026automated,
title = {{Automated Verification of Hamiltonian Simulation by Quantum Signal Processing}},
author = {Min Lai and Yu-Fang Chen and Shih-Han Hung},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.39491},
eprint = {2610.39491},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.39491},
}
RIS
TY - UNPB
TI - Automated Verification of Hamiltonian Simulation by Quantum Signal Processing
AU - Min Lai
AU - Yu-Fang Chen
AU - Shih-Han Hung
PY - 2026
DA - 2026/10/29
PB - arXiv
DO - 10.48550/arxiv.2610.39491
UR - https://arxiv.org/abs/2610.39491
AB - We present, to the best of our knowledge, the first fully automated verification framework for QSP-based Hamiltonian simulation. Our framework exploits the structure of the simulation algorithm: Hamiltonians are given as weighted sums of Pauli strings, embedded into larger unitaries through block encodings, and transformed into time-evolution operators by quantum signal processing (QSP). Using a symbolic Pauli-sum semantics for ancilla-indexed circuit blocks, our verifier proves that the distinguished all-zero ancilla block is proportional to the target Hamiltonian and infers the subnormalization factor automatically. It then verifies the QSP layer by extracting the implemented polynomial transformation and certifying its approximation error. This structure-aware abstraction is essential for scalability. Composing our verified block encoding and QSP wrapper yields an estimated macro-expanded size of about 1.52 million gates. The verifier certifies the block encoding once and checks the QSP layer through its abstract interface, without expanding the oracle calls. Our implementation verifies block encodings of structured Pauli-sum Hamiltonians with up to 256 system qubits and verifies QSP Hamiltonian-simulation instances by extracting their implemented polynomials and checking the resulting approximation bounds. These results show that fully automated verification can handle common Hamiltonian-simulation circuits at substantial scale when it exploits their algorithmic structure.
ER -