OEIS Open：语言模型能将多少猜想转化为定理？
文章背景与核心概要
本文介绍了 OEIS Open，这是一个旨在评估大语言模型（LM）解决开放数学问题能力的全新基准测试。该基准基于整数序列在线百科全书（OEIS）中 492 个已在 Lean 定理证明器中形式化的开放猜想，为通用语言模型提供了一个安全且开源的评估框架。
研究发现，在每次尝试 50 美元的预算下，配备极简工具的语言模型能够解决 147 个猜想（得分 30%）。在针对 100 个猜想的子集（OEIS Open Lite）中，表现最好的模型在 200 美元预算下达到了 44% 的准确率。令人意外的是，为模型提供 47.6 万篇 arXiv 数学论文的检索权限，或使用更复杂的智能体循环，均未能显著提升性能。尽管这些猜想的数学意义各异，但该研究证明了语言模型能够以较低的成本自主解决开放性的研究猜想。
执行摘要
本文介绍了 OEIS Open，这是一个旨在评估大语言模型（LM）解决开放数学问题能力的全新基准测试。该基准基于整数序列在线百科全书（OEIS）中 492 个已在 Lean 定理证明器中形式化的开放猜想，为通用语言模型提供了一个安全且开源的评估框架。
This paper introduces OEIS Open, a new benchmark designed to evaluate language models (LMs) on their ability to solve open mathematical problems. Built upon 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS) formalized in the Lean theorem prover, the benchmark provides a secure, open-source evaluation framework for generic LMs.
关键研究发现包括： * 在每次尝试 50 美元的预算下，配备极简工具的语言模型解决了 147 个猜想（得分 30%）。 * 表现最好的语言模型在 OEIS Open Lite（包含 100 个猜想的子集）上，以 200 美元的预算取得了 44% 的得分。 * 令人好奇的是，为模型提供 47.6 万篇 arXiv 数学论文的访问权限，或利用更复杂的智能体循环，均未能提升性能。 * 尽管这些特定猜想的数学意义各不相同，且许多猜想此前鲜有人关注，但研究结果表明，语言模型能够以适中的成本自主解决开放性的研究猜想。
Key findings include: * LMs with minimal tooling resolve 147 conjectures (30% score) under a budget of $50 per attempt. * The best-performing LM scores 44% on OEIS Open Lite (a 100-conjecture subset) with a $200 budget. * Curiously, granting models access to 476,000 arXiv mathematics papers or utilizing more sophisticated agent loops did not improve performance. * While the mathematical significance of these specific conjectures varies and many have received little prior human attention, the results demonstrate that LMs can autonomously resolve open research conjectures at a modest cost.
论文元数据
| 字段 | 详情 |
|---|---|
| arXiv ID | arXiv:2608.11941 [cs.AI] |
| 作者 | Tom Adamczewski |
| 提交日期 | 2026年8月12日（修订：2026年8月13日） |
| 学科 | 人工智能 (cs.AI) |
| MSC 分类 | 68V15 (主要), 68T07 |
| ACM 分类 | I.2.3; F.4.1 |
| 资源 | • 代码: GitHub - LeanOpenProblems • 结果: GitHub - LeanOpenProblems-results |
摘要
我们构建了 OEIS Open，这是一个基于 OEIS 中 492 个开放数学猜想的基准测试，这些猜想由 Tsoukalas 等人使用 Lean 进行了形式化。虽然这些猜想此前仅通过定制的智能体进行过尝试，但我们的开源评估代码允许任何通用语言模型（LM）针对这些问题进行测试，并能有效防止语言模型的作弊行为。
We construct OEIS Open, a benchmark based on 492 open mathematical conjectures from the OEIS, formalized in Lean by Tsoukalas et al. Whereas these conjectures had previously been attempted only with a bespoke agent, our open-source evaluation code runs any generic language model (LM) against them, and is secure against LM cheating attempts.
我们发现，配备极简工具集的语言模型在每次尝试 50 美元的预算下解决了其中的 147 个猜想，在 OEIS Open 上得分为 30%。OEIS Open Lite 是一个包含 100 个猜想的随机子集，用于更低成本的评估。当以每次尝试 200 美元的预算进行评估时，当前表现最好的语言模型在 OEIS Open Lite 上得分为 44%。通过 47.6 万篇 arXiv 论文为语言模型提供数学文献访问权限，或使用更复杂的智能体循环，均未能提高在 OEIS Open Lite 上的性能。
We find that LMs equipped with a minimal set of tools resolve 147 of these conjectures with a budget of $50 per attempt, scoring 30% on OEIS Open. OEIS Open Lite is a random subset of 100 conjectures for cheaper evaluation. When evaluated with a budget of $200 per attempt, the best current LM scores 44% on OEIS Open Lite. Giving LMs access to the mathematics literature via 476,000 papers from arXiv did not increase performance on OEIS Open Lite, and nor did using more sophisticated agent loops.
本研究涵盖的猜想其数学意义尚不确定，且大多数可能此前鲜有人关注。尽管如此，我们的结果表明，语言模型能够以适中的成本自主解决开放性的研究猜想。
The conjectures covered in this work are of uncertain mathematical significance, and most have likely received little previous attention. Nevertheless, our results show that LMs can resolve open research conjectures autonomously and at modest cost.
