解决（部分）形式化数学奥林匹克问题

# 解决（部分）正式数学奥林匹克问题 来源：https://openai.com/index/formal-math/ 我们在 miniF2F（https://arxiv.org/abs/2109.00110）基准测试上取得了最新的最先进成绩（41.2% vs 29.3%），这是一个具有挑战性的高中奥林匹克问题集合。我们的方法称为**陈述课程学习**，包括手动收集一组难度各异的陈述（不包括证明），其中最难的陈述类似于我们的目标基准。最初，我们的神经证明器很弱，只能证明其中少数几个。我们迭代地搜索新的证明，并在新发现的证明上重新训练我们的神经网络，经过 8 次迭代后，我们的证明器在 miniF2F 测试中表现得极其出色。 形式数学是一个令人兴奋的研究领域，因为：(i) 它的丰富性，允许你证明任意的定理，这些定理需要推理、创意和洞察力；(ii) 它与游戏的相似性——人工智能在游戏领域取得了巨大成功——在于它有一种自动化的方式来确定证明是否成功（即由形式系统验证）。如下面的琐碎例子所示，证明一个形式陈述需要生成一系列证明步骤，每个证明步骤包括对一个策略的调用。B（https://openai.com/index/formal-math/#citation-bottom-B） 这些策略以数学术语作为参数，每个策略调用将把当前需要证明的陈述转换为更容易证明的陈述，直到没有任何东西需要证明为止。