人机协作进化发现纠缠辅助量子码族

从有限构造到可证明的码族

大语言模型（LLM）引导的程序进化能够生成数学构造，但构造的有效性、通用性和可复现性需要不同类型的证据。近期一项研究提出了一种“研究者参与循环”（researcher-in-the-loop）的发现流程，将程序进化、精确评估、数学推广、不存在性认证检查与形式化证明检查结合起来，并应用于纠缠辅助量子纠错码（EAQECC）的发现。该工作展示了如何将有限的计算发现转化为具有独立可检验证据的数学定理，为AI辅助数学发现提供了可复用的范式。

研究流程示意图

核心方法：五步证据链

该流程的核心在于构建一条完整的证据链，每一步都有独立的验证机制：

程序进化：从没有指定族公式的任务出发，利用LLM引导的进化算法生成候选程序。这些程序输出有限的量子比特构造，而非直接的代数表达式。
精确评估：对生成的构造进行精确的数值评估，确保其满足纠缠辅助量子纠错码的基本参数要求。
数学推广：研究者分析有限构造的结构，将其推广为一般的族公式。在此案例中，研究者将结构推广为 $[[n,1,n-1;n-q-1]]_q$ 族，适用于素数幂 $q\ge3$ 且 $n\ge2q+1$ 的情形，以及 $q=2$ 且奇数 $n\ge5$ 的情形。
不存在性认证：通过DRAT证明检查，验证某些参数下码不存在，提供了115个已验证码记录和10个带检查DRAT证明的不存在性结果。
形式化证明检查：使用Lean定理证明器检查该族背后的代数证书，确保数学推导的严谨性。

这种多层次的验证策略，使得AI生成的数学发现不再停留在“有趣但未经证实”的阶段，而是具备了可发表级别的严谨性。

纠缠辅助量子纠错码（EAQECC） 是标准量子纠错码的推广，允许编码器与解码器共享预先纠缠的量子比特对（ebits），从而突破标准量子码的 Singleton 界等限制。其参数通常记为 $[[n,k,d;c]]_q$，其中 $n$ 为物理量子比特数、$k$ 为逻辑量子比特数、$d$ 为最小距离、$c$ 为消耗的纠缠比特数，$q$ 为有限域大小。纠缠辅助可以换取更高的编码效率或更大的距离，但需要消耗额外的纠缠资源，因此存在编码增益与纠缠开销之间的权衡。该研究发现的 $[[n,1,n-1;n-q-1]]_q$ 族即描述了这种权衡的具体实例。

DRAT（Deletion Resolution Asymmetric Tautology）证明 是 SAT 求解器输出的一种可机器检查的证明格式。当求解器判定某个布尔公式不可满足时，它可生成一系列子句添加与删除步骤；独立的 DRAT 检查器验证每一步是否保持可满足性，从而确认原公式确实无解。在本研究中，码不存在性的验证被编码为 SAT 问题，若求解器返回“不可满足”，则其 DRAT 证明经检查后即可作为不存在性的严格证书。这比仅依赖求解器输出更具可信度，因为证明可被第三方独立复核，而不必信任求解器本身的正确性。

Lean 定理证明器 是一个基于依值类型论的交互式形式化证明助手，其数学库 Mathlib 已覆盖大量现代数学内容。在 Lean 中，每一个证明最终都被转化为一系列可由内核自动检查的推理步骤，因此只要证明通过编译，就排除了隐含假设或计算错误。本研究使用 Lean 检查该码族背后的代数证书，意味着族公式的推导（而不仅是有限实例）获得了形式化保证。这补足了数值评估与 SAT 不存在性证明之间的缺口，使“有限构造→一般族”的推广步骤也具备可独立检验的证据。

实验数据与性能对比

研究团队在受控的八组配对生成块中进行了实验，比较了验证集选择的迭代程序与独立生成程序在未见长度 $n=13,15$ 上的表现。结果显示，迭代程序在留出执行中的成功率分别为46.1%和31.6%，而独立生成程序仅为19.5%和3.1%。这一显著差异表明，程序进化结合研究者分析能够有效提升发现的泛化能力。

此外，结合纠缠提升技术，该码族填补了存档EAQECC表中的54个空白。这些结果不仅验证了方法的有效性，也展示了AI在数学构造发现中的实际贡献。

程序进化中的迭代与独立生成 是两种不同的搜索范式。独立生成指每次从零开始运行进化算法，各次运行之间不共享信息；迭代程序则将上一轮验证集上表现最好的候选程序作为下一轮的起点，逐步积累有效结构。在未见长度上的成功率差异（46.1% vs 19.5%、31.6% vs 3.1%）反映了迭代机制带来的泛化优势：程序并非记住特定 $n$ 的构造，而是学到了可迁移的构造模式。这一对比设计控制了生成长度，使成功率差异可归因于进化策略而非任务难度。

可复现性与证据发布

该研究强调可复现性，发布了完整的证据包，包括：

115个已验证的码记录
10个带检查DRAT证明的不存在性结果
族实现代码
保留的搜索程序，用于精确检查和种子化重放

这种开放证据的做法，使得其他研究者能够独立验证结果，并在此基础上进行进一步探索。

意义与展望

这项工作将LLM引导的程序进化与严格的形式化验证相结合，为AI辅助数学发现提供了一条可行的路径。研究者参与循环的流程既发挥了AI在搜索空间探索上的优势，又保留了人类研究者在模式识别和数学推广中的关键作用。随着形式化工具的成熟和LLM能力的提升，类似的流程有望应用于更广泛的数学领域，加速从计算实验到数学定理的转化。