OEIS Open：语言模型能把多少猜想变成定理？

我们构建了OEIS Open，一个基于OEIS中492个开放数学猜想的基准，这些猜想已由Tsoukalas等人在Lean中形式化。此前这些猜想仅用定制智能体尝试过，而我们的开源评估代码可以让任何通用语言模型（LM）对其求解，且能防范LM的作弊尝试。我们发现，配备最小工具集的语言模型在每次尝试50美元的预算下解决了其中147个猜想，在OEIS Open上得分30%。OEIS Open Lite是从中随机抽取的100个猜想子集，用于更廉价的评估。在每次尝试200美元的预算下评估时，当前最佳语言模型在OEIS Open Lite上得分44%。让语言模型访问来自arXiv的476,000篇论文构成的数学文献并未提升其在OEIS Open Lite上的表现，使用更复杂的Agent循环也是如此。本工作覆盖的猜想数学意义尚不确定，且大多数此前可能很少受到关注。尽管如此，我们的结果表明语言模型能够以适度成本自主解决开放研究猜想。