研究者观察到，生成策略参数所需的原始数学术语的能力出现在了他们的训练过程中，这是离开神经语言模型所无法完成的。下面的证明就是它的一个例子：证明步骤「use n + 1」（完全由模型生成）提出使用「n + 1」作为解决方案，剩下的形式证明依赖于「ring _ exp」策略来验证它确实有效。
研究者还观察到，他们的模型和搜索过程能够产生链接多个重要推理步骤的证明。在下面的证明中，模型首先使用了引出存在性命题（existential statement） (∃ (x : ℝ), f x ≠ a * x + b) 的换质换位律（contraposition）。然后，它使用 use (0 : ℝ) 为它生成一个 witness，并通过利用 norm _ num 策略来完成证明。
该模型经过 statement curriculum learning 的训练，能够解决培训教材以及 AMC12 和 AIME 中的各种问题，以及改编自 IMO 的两个问题。下面是三个有关的例子。
形式数学涉及两个主要的挑战，使得单纯的强化学习应用不太可能成功：
1. 无限的动作空间：形式数学不仅有超大的搜索空间（比如像围棋），还有无限的动作空间。在搜索证明的每个步骤，模型的选择范围不是一组行为良好的有限动作，而是一组复杂且无限的策略，涉及必须生成的外生数学术语（例如，生成用作 witness 的数学命题)。
2. 缺乏自博弈（self-play）：与两人游戏相反，证明器不是与对手对抗，而是与一系列需要证明的命题对抗。当面对一个过于困难的命题时，没有明显的重构可以让证明器首先生成更容易处理的中间语句。这种不对称性阻止了在双人游戏中获得成功的自博弈算法的简单应用。
在这项工作中，研究者通过从一个语言模型中采样动作来解决无限动作空间问题。语言模型能够生成策略调用以及通常需要作为参数的原始数学术语。对于自博弈的缺乏，他们观察到，自博弈在两人游戏中的关键作用是提供一个无监督的课程（curriculum）。因此，他们建议用一套不同难度的辅助问题命题（不需要证明）来代替这种无监督的课程。他们的实验结果表明，当这些辅助问题的难度变化足够大时，他们的训练程序就能够解决一系列越来越难的问题，最终推广到他们所关心的问题集。
虽然这些结果非常令人兴奋，因为它们证明了深度学习模型在与形式系统交互时能够进行重要的数学推理，但在竞赛中，该证明器离最佳学生表现还差得很远。研究者表示，他们希望自己的工作将推动这一领域的研究，特别是针对 IMO 的研究，并希望他们提出的 statement curriculum learning 方法能够加快自动推理的研究进展。
**小结**
两家机构最新的研究成果已经介绍完毕，网上已经零零散散地出现了关于效果的评价：
如有 AI 研究科学家发系列长推表示，AlphaCode 达到人类水平还需要几年时间，它在 codeforce 上的排名是有限制的，如许多参与者是高中生或大学生；还有就是 AlphaCode 生成的绝大多数程序都是错误的，正是使用示例测试进行过滤才使得 AlphaCode 实际解决了某些问题。
也有研究人员表示，这像是 AlphaStar 大力出奇迹的结果。
国内的 AI 从业者们可以趁假期研究下这两项研究，发表自己的看法。
