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.

The paper addresses automated verification that a block-encoding/QSP circuit approximates $e^{-iHt}$ for a Hamiltonian specified as a weighted Pauli sum, without constructing its matrix or supplying a reference circuit. The guarantee concerns the circuit’s principal ancilla block $B$: $\|\beta B-e^{-iHt}\|\leq\epsilon$, allowing an inferred normalization $\beta$ rather than requiring deterministic time evolution. Verification is compositional. Ancilla-indexed symbolic execution tracks Pauli-sum system operators, checks the block encoding, and infers its normalization $\alpha$. The QSP layer then uses a four-block symbolic abstraction of the certified unitary; unitarity-derived rewrites extract its implemented polynomial. Least-squares normalization and residual checks at Chebyshev nodes certify uniform approximation, with grid size $O(|\alpha t|+\log(1/\epsilon)+d)$. Soundness combines polynomial approximation error with $|t|\epsilon_{\mathrm{BE}}$. The implementation uses 60-digit ball arithmetic. The evaluation verifies 50 of 51 structured block encodings within 1,800 seconds, including 256-qubit, 512-term instances. The largest Heisenberg case completes in 4,976 seconds under an extended timeout. All 50 QSP benchmarks pass, reaching degree 77 at effective time 50, verified in approximately three seconds. Composing the largest Ising encoding with that wrapper gives an estimated 1.52-million-gate circuit, excluding additional control-decomposition overhead. Testing also identifies a padding-related block-encoding bug in Cobble. Supported circuit languages restrict ancilla/system interactions and QSP access to nonzero ancilla branches. Symbolic expressions can grow exponentially, and rewriting is incomplete outside standard QSP forms. Oblivious amplitude amplification is not verified.