自动化数学理论形成中的有趣度学习

我们在自动发现新数学理论这一人工智能的宏大挑战中迈出了两个关键步骤。首先，我们引入 $\emph{FERMAT}$，一个使用符号动作建模概念发现和定理证明的强化学习 (RL) 环境，开启了一系列与理论发现相关的 RL 问题。其次，我们通过 $\emph{FERMAT}$ 探索了一个具体问题：自动对数学对象进行有趣度评分。我们研究了用于合成非平凡有趣度度量的进化算法。特别是，我们引入一个基于 LLM 的进化算法，具有函数抽象特性，在发现初等数论和有限域方面显著优于硬编码基准。我们在本篇论文中开源了 $\emph{FERMAT}$ 环境。