用于认证量子神经网络设计的智能形式化
An Agentic Formalization for Certified Quantum Neural Network Design
AI总结：
该研究聚焦量子神经网络设计中表现力与可训练性平衡问题，通过连通精益4开发形式化QNN理论主要组件，在表现力和可训练性方面分别取得成果，还明确了相关修正与澄清，为QNN理论提供机器可检查基础，助力量子机器学习算法设计。
AI中文摘要：
量子机器学习中的核心模型是量子神经网络（QNN），其设计需要平衡表现力和可训练性。在技术上，表现力通过电路函数分析来研究，可训练性则使用动态李代数（DLA）方法进行分析。为支持经过认证的QNN设计，我们在由证明内核检查的连通精益4开发中对QNN理论的这些主要组件进行形式化，其中每个分析输入要么被证明，要么作为命名假设公开。在表现力方面，我们证明了单量子比特QNN的当且仅当精确特征、资源计数量子相位处理定理以及通过DLA维度限制量子费舍尔信息秩的过参数化上限。在可训练性方面，我们通过去循环化的二阶矩接口推导出直和损失方差定律。一个参数化的卡西米尔唯一性引擎为完全可控、正交和匹配门电路族提供所需输入，而单量子比特和乘积克利福德集合直接封闭两个设计假设。一个顶点定理将条件方差定律与DLA坐标中的精确损失重建配对。开发记录确定了八个在非正式论证中未明确的修正和澄清。我们期望这项工作为QNN理论提供一个机器可检查的基础，并朝着量子机器学习算法的人工智能辅助或自动化设计迈出一步。
英文摘要：
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.
