Alien Coding
Thibault Gauthier, Miroslav Olšák, Josef Urban
cs.AI, cs.LG, cs.LO, cs.NE, math.NT
2023-01-27
NMT 把数列翻译成程序，验证后回流训练；从随机代码起步，190 轮解出 78,118 条 OEIS 数列，累计 84,587 条。
OEIS 是整数数列在线百科全书，35 万余条目各含一个数列和人类描述，约三分之一附有生成程序。这篇的问题很纯粹：不看任何人类代码，系统能不能从随机程序起步，自己给数列发明生成程序。自动定理证明界长期只练「学习引导证明搜索」，猜猜想、提解释没人碰；整数数列是干净的试验场，任何候选解释(一段程序)都能被机械验证。同团队前作用树神经网络加 MCTS,25 轮解出 27987 条；这篇换掉两个核心组件，把循环推到极限。
系统循环跑三个阶段：搜索、检查、学习。
编程语言只有 14 个 token,刻意极简以避开人类偏见，又靠 compr 算子(返回第 n 个满足谓词的非负整数，相当于递归函数论里的 µ 算子)做到图灵完备。斐波那契一行写完：loop2(x+y, x, x, 0, 1);素数数列就是素数判定谓词接 compr。
同时留最短和最快两套解是关键设计：短程序可能慢到无法在时限内验证，验证不了就没有训练数据；快程序是更复杂程序的构件，已解数列的最快版本随后续迭代持续提速。后期再叠三招：并行训 24 个吃不同数据子集的模型做组合推理(portfolio)、跨轮连续训练(累计超 140 万步)、检查从 hybrid 切到全量慢检查。
| 设置 | 轮次 | 解出数列 |
| 随机起步 | 0 | 3,771 |
| TNN 基线(前作架构) | 500 | 末期每轮仅增约 5 条，饱和 |
| nmt0(单 NMT 模型，约 1 个月) | 100 | 46,707 |
| nmt1(多模型组合，4 卡 3 个月) | 190 | 78,118 |
| 所有实验累计(截至 2023 年 1 月) | — | 84,587 |
第 21 轮引入组合模型后，单轮新增 687 条，单模型同期只有 272 条；第 159 轮把检查换成慢检查(45 分钟变 6 小时)，单轮新增从 178 跳到 860,多是 compr 类程序获放行。nmt1 跑到 190 轮，单轮新增仍很少低于 200,nmt0 和 TNN 都见到的平台期在它身上没有出现。
泛化检验最能说明问题：78,118 个解中有 40,577 条在 b-file 里另附 100 个更长的项。未超时的程序里，最短解 90.57% 能续写正确，最快解只有 77.51%,失败常见于依赖 π 这类实数的近似。累计 84,587 条，是前作 27,987 的三倍多。
这是「学习-搜索-验证」正反馈在图灵完备、无封顶任务上的规模化样本。Go、Chess 那类自博弈环境表达力有上限，这里的语言原则上能写出任意算法。
所有解都是可解释、被机械验证过的符号程序。作者明确说，若让网络直接预测每个数列的后 100 项，系统根本无法自举，符号表示才是泛化与自我学习的根基。一个产出对照全部目标、双适应度(短+快)、portfolio 加连续训练，这套组合可以迁到别的合成任务上。系统还自己长出 20 多种(伪)素数定义，重新发明了把两个变量打包成一个数的配对函数。定位也要诚实：4 卡 GPU 跑 3 个月换 7.8 万条解，这是研究装置，不是即用产品。
作者自认的：宏(定义复用)实验效果不明，nmt2、nmt3 各比 nmt1 多不到 2,800 条解，与 DreamCoder「定义带来收益」的说法对不上，且两个跑都没满 100 轮，比较只是初步；与同期监督式工作(在 1 万条简单数列上报精度)和预训练代码模型(1 万条里解出 11.5%)没有直接可比的对照。
另有两处冷水：「解出」只意味着程序复现了词条列出的有限几项，放到 100 个更长项上，未超时的最快解约 22% 对不上，拟合前缀不等于找到真解释；84,587 对 351,663 的覆盖率约四分之一，剩下的难在语言表达力还是搜索算力，论文没有分析。