Concepts formalized in this paper.Abstract
A central model in quantum machine learning is the quantum neural network (QNN), whose design requires balancing expressivity and trainability. Technically, expressivity is studied through circuit-function analysis, such as quantum signal processing, while trainability is analyzed using dynamical-Lie-algebra (DLA) methods. To support certified QNN design, we formalize these major components of QNN theory in a connected lean 4 development checked by a proof kernel, where every analytic input is either proved or exposed as a named hypothesis. On the expressivity side, we prove exact if-and-only-if characterizations of single-qubit QNNs, a resource-counted quantum phase processing theorem, and an overparameterization ceiling that bounds the quantum Fisher information rank by the DLA dimension. On the trainability side, we derive the direct-sum loss-variance law through a de-circularized second-moment interface. A parameterized Casimir-uniqueness engine discharges the required inputs for fully controllable, orthogonal, and matchgate circuit families, while single-qubit and product-Clifford ensembles close the two-design assumptions directly. A capstone theorem pairs the conditional variance law with exact loss reconstruction in DLA coordinates. The development record identifies eight corrections and clarifications that were not explicit in the informal arguments. We expect this work to provide a machine-checkable foundation for QNN theory and a step toward AI-assisted or automated design of quantum machine learning algorithms.
Mingrui Jing
PhD Student (2023)
I obtained my BS and MS degrees in physics from the University of Melbourne. My research interests include distributed quantum computing, quantum entanglement and quantum machine learning.
Lei Zhang
PhD Student (2023)
I obtained my BMath in AMath, CO & joint PMath from the University of Waterloo. My research interests include quantum algorithm design and quantum machine learning.
Hongshun Yao
PhD Student (2024)
I obtained my BS degree in Mathematics from Nanjing University of Aeronautics and Astronautics and my MS degree in Mathematics from Beihang University. My research interests include quantum information theory and quantum machine learning.
Xin Wang
Associate Professor
Prof. Xin Wang founded the QuAIR Lab at HKUST (Guangzhou) in June 2023. His research aims to advance our understanding of the limits of information processing with quantum systems and the potential of quantum artificial intelligence. His current interests include quantum algorithms, quantum resource theory, quantum machine learning, quantum computer architecture, and quantum error processing. Prior to establishing the QuAIR Lab, Prof. Wang was a Staff Researcher at the Institute for Quantum Computing at Baidu Research, where he focused on quantum computing research and the development of the Baidu Quantum Platform. Notably, he led the development of Paddle Quantum, a Python library for quantum machine learning. From 2018 to 2019, he was a Hartree Postdoctoral Fellow at the Joint Center for Quantum Information and Computer Science (QuICS) at the University of Maryland, College Park. Prof. Wang received his Ph.D. in quantum information from the University of Technology Sydney in 2018, under the supervision of Prof. Runyao Duan and Prof. Andreas Winter. He obtained his B.S. in mathematics (Wu Yuzhang Honors) from Sichuan University in 2014.