摘要

本文探讨了如何从数学公理中发现数学定理的柏拉图式观点，并描述了MINIMO（从内在动机出发的数学）：一个同时学习提出挑战性问题（猜想）和解决这些问题（定理证明）的代理。给定一个在依赖类型理论中公理化的数学领域，我们首先结合受限解码和类型导向合成的方法，从语言模型中采样有效的猜想。我们的方法保证了猜想的良好形式化，即使在模型随机初始化的情况下也是如此。我们使用相同的模型来表示证明搜索的策略和价值函数。我们的代理目标是生成难以证明但可证明的猜想——这是一个移动目标，因为代理自身的定理证明能力也在训练过程中提高。我们提出了在证明搜索树上进行事后重标记的新方法，以显著提高代理在两个任务中的样本效率。实验在三个公理化领域（命题逻辑、算术和群论）中进行，表明我们的代理可以从仅有的公理出发，自我改进，生成真实且具有挑战性的猜想并找到证明。

原理

MINIMO的核心工作原理是结合受限解码和类型导向合成的方法，从语言模型中生成有效的猜想。这种方法确保了猜想的良好形式化，即使在模型随机初始化的情况下也是如此。具体来说，代理使用一个Transformer语言模型，该模型在初始阶段是随机初始化的。通过受限解码和类型导向合成，代理能够生成符合依赖类型理论的猜想。此外，代理使用相同的模型来表示证明搜索的策略和价值函数，从而指导证明搜索过程。当找到证明时，证明搜索会生成用于改进策略和价值的训练数据；同时，这些数据也用于改进猜想生成，因为代理可以了解问题的难度。通过这种交替进行猜想生成和定理证明的自我改进循环，代理能够不断提出更难但可证明的猜想，并找到它们的证明。

流程

MINIMO的工作流程包括以下几个关键步骤：

1. 猜想生成：代理使用Transformer语言模型生成猜想。通过受限解码和类型导向合成，代理能够生成符合依赖类型理论的有效猜想。
2. 证明搜索：代理使用蒙特卡洛树搜索（MCTS）进行证明搜索，该搜索由学习到的策略和价值函数指导。证明搜索在Peano环境中进行，该环境提供了一个有限的行动空间。
3. 事后重标记：当证明搜索失败时，代理使用事后重标记方法，将失败的轨迹重新标记为目标，从而生成训练数据。这显著加速了学习过程，使得代理能够从失败的证明搜索中提取数百个新的（真实的）猜想及其证明。
4. 训练循环：代理交替进行猜想生成和证明搜索，并使用生成的数据训练底层语言模型。这个过程形成了一个自我改进的循环，代理从仅有的公理出发，不断改进其猜想生成和定理证明的能力。

应用

MINIMO的应用前景广泛，特别是在需要数学证明的领域，如程序和硬件验证。代理能够从仅有的公理出发，自我改进，生成真实且具有挑战性的猜想并找到证明，这为自动化数学推理和证明提供了新的可能性。此外，MINIMO的方法还可以扩展到其他需要复杂推理和证明的领域，如人工智能安全和复杂系统分析。