An Agentic Formalization for Certified Quantum Neural Network Design

Research Question and Approach

Quantum neural networks (QNNs) are central to quantum machine learning, yet their design is often hampered by a tension between expressivity (the ability to represent complex functions) and trainability (the ability to optimize parameters without encountering barren plateaus). Existing theoretical frameworks for these properties often rely on informal derivations that can contain subtle gaps or unstated assumptions. This paper addresses this by formalizing QNN theory in Lean 4, an interactive theorem prover. The authors develop a connected, machine-checkable framework where every analytic input is either formally proved or explicitly declared as a named hypothesis, ensuring that the entire derivation chain is auditable by a proof kernel.

The authors successfully formalize two primary theoretical stacks: expressivity and trainability. On the expressivity side, they provide exact if-and-only-if characterizations for single-qubit QNNs, a resource-counted quantum phase processing theorem, and an overparameterization ceiling that bounds the quantum Fisher information rank by the dimension of the dynamical Lie algebra (DLA). On the trainability side, they derive the direct-sum loss-variance law, which relates loss concentration to the DLA structure. A capstone theorem links this variance law with exact loss reconstruction in DLA coordinates. By subjecting these theories to the rigor of a proof kernel, the authors identified and corrected eight clarifications and errors that were not explicit in the informal mathematical arguments.

This work moves quantum machine learning theory toward a more robust, verifiable foundation. By replacing informal "folklore" derivations with machine-checked proofs, the authors provide a reliable toolkit for circuit designers. This framework not only ensures the correctness of existing results but also serves as a template for AI-assisted formalization, potentially enabling the automated design of quantum algorithms with certified performance guarantees.