用多智能体系统设计量子纠错码，实现精确验证与形式化证明。
Co-Designing Quantum Codes with Transversal Diagonal Gates via Multi-Agent Systems
- 结合符号合成与形式化验证，构建可信赖的量子码搜索平台。
- 在距离2下发现14,116个精确编码，支持逻辑阶数2至18。
- 首次在距离3中解决T门透射问题，结果经Lean系统严格验证。
精确科学发现不能仅依赖启发式搜索：候选构造必须转化为精确对象并独立验证。本文通过在TeXRA基础上增加独立的Lean 4验证层，构建了一个人工引导的多智能体平台，用于精确科学发现。该平台整合符号合成、组合与线性规划搜索、数值候选的精确重构及形式化验证。我们将其应用于具有指定透射对角门的非加性量子纠错码，在子集和线性规划（SSLP）框架下研究。在距离2情形中，当逻辑态位于不同剩余类时，平台生成了14,116个代码（$K\{2,3,4\u007d$，最多6个物理量子比特），实现逻辑循环阶数2至18，并从中提取出闭式无限族。此外，构造出一个残余退化的$((6,4,2))$码，实现逻辑受控相位门${\mathrm{diag}(1,1,1,i)\u007d$。在距离3情形下，我们在互补二元二面体${\mathrm{BD}_{16}\u007d$设置中解决了$((7,2,3))$码的透射-T问题：12个候选经SSLP筛选后，10个可精确实现，2个被无解证明排除。所有构造、族及无解结果均在Lean中形式化并验证，展示了人工智能辅助工作流如何连接搜索、精确重构与形式证明。
原文摘要 · Abstract (English)
Exact scientific discovery requires more than heuristic search: candidate constructions must be turned into exact objects and checked independently. We address this gap by extending TeXRA with an independent Lean 4 verification layer, turning it into a human-guided multi-agent platform for exact scientific discovery. The platform couples symbolic synthesis, combinatorial and linear-programming search, exact reconstruction of numerical candidates, and formal verification in Lean. We apply this platform to nonadditive quantum error-correcting codes with prescribed transversal diagonal gates within the subset-sum linear-programming (SSLP) framework. In the distance-2 regime where logical states occupy distinct residue classes, the platform yields a Lean-certified catalogue of 14,116 codes for $K\in\{2,3,4\}$ and up to six physical qubits, realizing cyclic logical orders 2 through 18, from which we extract closed-form infinite families. We also construct a residue-degenerate $((6,4,2))$ code implementing the logical controlled-phase gate $\mathrm{diag}(1,1,1,i)$. At distance 3, we resolve the transversal-$T$ problem for $((7,2,3))$ codes within the complementary binary-dihedral $\mathrm{BD}_{16}$ setting: among the 12 candidates surviving the SSLP filters, 10 admit exact realizations and 2 are excluded by no-go proofs. All accepted constructions, families, and no-go results are formalized and checked in Lean, illustrating how AI-assisted workflows can bridge search, exact reconstruction, and formal proof in the physical sciences.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。