研究者参与的LLM程序演化发现并验证量子纠错码族

LLM 引导的程序演化可以产生数学构造，但有效性、一般性和可重复性需要分别提供证据。我们开发了一个研究人员在环发现管道，结合了程序演化、精确评估、数学概括、经过认证的不存在检查和形式证明检查。我们将其应用于纠缠辅助量子纠错码（EAQECC）。从没有指定码族公式的任务开始，进化程序产生了有限的量子位结构，其结构研究人员将素数幂 $q\ge3$ 的 $n\ge2q+1$ 和 $q=2$ 的奇数 $n\ge5$ 推广到码族 $[[n,1,n-1;n-q-1]]_q$。Lean检查该族的代数证书。与纠缠提升一起，该系列弥补了存档的 EAQECC 表中的 54 个空白。已发布的证据包括 115 个经过验证的量子纠错码记录、10 个经过检查的 DRAT 证明的不存在结果、系列实现以及用于精确检查和种子重放的保留搜索程序。在八个配对生成块的受控队列中，由验证集选择的迭代程序在未见长度 $n=13,15$ 的保留执行中取得了 46.1% 和 31.6% 的成功，而独立生成的程序的成功率为 19.5% 和 3.1%。在这种情况下，程序演化和研究人员分析将有限的计算发现转变为具有独立可检查证据的经过验证的码族。