研究者参与的纠缠辅助量子码族演化发现

大语言模型引导的程序演化能够产生数学构造，但其有效性、一般性和可复现性需要不同的证据支持。我们开发了一套研究者参与的发现流程，将程序演化、精确评估、数学推广、经认证的不存在性检验和形式化证明检查相结合。我们将其应用于纠缠辅助量子纠错码（EAQECCs）。从未指定码族公式的任务出发，演化生成的程序产生了有限的量子比特码构造，研究者将其结构推广为码族 $[[n,1,n-1;n-q-1]]_q$，适用范围为素数幂 $q\ge3$ 且 $n\ge2q+1$，以及 $q=2$ 且 $n\ge5$ 为奇数的情形。Lean 检查了支撑该码族的代数证书。结合纠缠提升，该码族填补了已归档 EAQECC 表中的 54 个空缺。公开的证据包括 115 条已验证的码记录、十项附有已检查 DRAT 证明的不存在性结果、码族实现，以及保留下来的搜索程序，可用于精确检查和基于随机种子的重放。在由八组成对生成区块构成的受控实验中，经验证筛选的迭代程序在未见过的长度 $n=13,15$ 上，留出测试执行的成功率分别达到 46.1% 和 31.6%，而独立生成程序的相应成功率为 19.5% 和 3.1%。在这一设定下，程序演化与研究者分析将有限的计算发现转化为一个经过证明的码族，并提供了可独立核验的证据。