基于内在动机的形式数学学习

人类是如何从太虚中探寻出数学的？我们探索了柏拉图主义的观点，即数学可以从其公理中被发现——一场猜想与证明的游戏。我们描述了 Minimo（基于内在动机的数学）：一个联合学习为自身提出挑战性问题（猜想）并解决它们（定理证明）的智能体。给定一个以依值类型理论公理化的数学领域，我们首先结合约束解码和类型导向合成的方法，从语言模型中采样有效的猜想。我们的方法在构造上保证了猜想的良构性，即使我们从一个随机初始化的模型开始也是如此。我们使用同一个模型来表示用于引导证明搜索的策略和价值函数。我们的智能体旨在生成困难但可证明的猜想——这是一个移动的目标，因为其自身的定理证明能力也会随着训练而提高。我们提出了在证明搜索树上进行事后重新标记的新方法，以显著提高智能体在两项任务中的样本效率。在 3 个公理化领域（命题逻辑、算术和群论）上的实验表明，我们的智能体可以仅从公理进行自举，在生成正确且具有挑战性的猜想和寻找证明方面实现自我改进。