微软资助的OpenAI同天发布了能够证明数学竞赛题的神经网络

//OpenAI实际上是独立的工作室，但微软领投了10亿美元。而且，这次发布的神经网络基于由微软研究中心工作人员开发但和微软没关系的程序证明校验语言Lean。

我们为Lean构建了一个神经定理证明器，它学会了解决各种具有挑战性的高中奥林匹克问题，包括 AMC12 和 AIME (美国中学生数学联赛)的问题，以及改编自IMO(国际中学生数学奥林匹克竞赛)的2个问题。

证明器使用语言模型来寻找形式陈述的证明。每次我们找到一个新的证明时，我们都会将其用作新的训练数据，这会改进神经网络并使其能够迭代地找到更难问题的证明方案。

我们在 miniF2F 基准测试中取得了新的最先进水平(41.2% vs 29.3%)，这是一个具有挑战性的高中奥林匹克问题集。我们的方法，我们称之为 陈述课程学习，包括手动收集一组不同难度级别的命题(没有证明)，其中最难的命题与我们的目标基准相似。

最初，我们的神经网络证明器很弱，只能证明其中的几个。我们反复搜索新的证明，并在新发现的证明上重新训练我们的神经网络，经过8次迭代，我们的证明者最终在 miniF2F 上测试时拿到了不错的成绩。

会用柯西不等式的AI

形式数学是一个令人兴奋的研究领域，因为

(i) 它的丰富性，让您可以证明需要推理、创造力和洞察力的任意定理，以及

(ii) 它与游戏的相似性——人工智能在游戏领域取得了惊人的成功——因为它具有自动化确定证明是否成功的方法(即，由正式系统验证)。如下面的简单示例所示，正式陈述需要生成一系列证明步骤，每个证明步骤都包含对策略的调用。

正式系统接受的工件语句是底层的(如汇编代码)，人类难以生成。策略是从更高级别的指令生成此类工件以帮助形式化的搜索过程。

我们观察到，在我们的训练过程中出现了生成作为战术参数所需的原始数学术语的能力，如果没有神经语言模型，这是无法完成的。在一个证明里，证明器基本掌握了数学归纳法的表述。

我们还观察到，我们的模型和搜索程序能够生成链接多个非平凡推理步骤的证明。在证明中，模型首先使用导致存在性陈述 (∃ (x : ℝ), f x ≠ a * x + b) 的对立。然后它使用 (0 : ℝ) 为它生成一个特例，并通过利用norm_num策略完成证明。

我们的模型经过陈述课程学习训练，能够解决培训教科书以及 AMC12 和 AIME 比赛中的各种问题，以及改编自 IMO 的 2 个问题。

但形式数学涉及两个主要挑战，使得强化学习的简单应用不太可能成功。

(i) 无限的动作空间：形式数学不仅有一个非常大的搜索空间(比如围棋)，它也有一个无限的动作空间。在证明搜索的每一步，模型必须不是从行为良好的有限动作集中进行选择，而是从一组复杂且无限的策略中进行选择，其中涉及必须生成的外生数学术语(自己定义符号，用作诸如“存在一个 xx st ...”之类的步骤中使用的对象，或在证明中间引入和链接引理)。

(ii) 缺乏自我博弈：与 2 人游戏相反，证明者不是与对手对抗，而是与一组要证明的陈述对抗。当面对一个太难的陈述时，没有明显的重构可以让证明器生成中间更容易解决的引理。这种不对称性阻止了在 2 人游戏中成功的自我游戏算法的幼稚应用。

在我们的工作中，我们通过在搜索证明时从语言模型中采样动作来解决无限动作空间问题。语言模型能够生成策略调用以及通常需要作为参数的原始数学术语。我们解决缺乏自我游戏的基础是观察到自我游戏在 2 人游戏中的关键作用是提供无监督的课程。我们建议用一组不同难度的辅助问题陈述(不需要证明)来代替这种无监督的课程。我们的经验表明，当辅助问题的难度足够时，我们的训练程序能够解决越来越难的问题，最终推广到我们关心的问题集。

虽然这些结果非常令人兴奋，因为它们证明了深度学习模型在与正式系统交互时能够进行非平凡的数学推理，但AI距离最出色的人类中学生还差得远，只是偶尔能，而非始终如一地解决具有挑战性的奥林匹克问题。尽管如此，我们希望我们的工作能够激发该领域的研究，特别是针对 IMO 大挑战，并且我们提出的陈述式课程学习方法将有助于加速自动化推理的总体进展。

论文 https://cdn.openai.com/papers/Formal_Mathematics_Statement_Curriculum_Learning__ICML_2022.pdf

https://openai.com/blog/formal-math/