SqueezeBench：抗饱和的数学能力评测基准

查看 PDF HTML（实验性）

摘要：AI 系统在数学领域正快速进步，但这种进步很难衡量。已解问题的基准测试趋于饱和，而在开放问题的基准测试中，每个问题只能被首次解决一次。我们提出 SqueezeBench，一个对饱和具有韧性的基准测试：一次成功会提高门槛，而不是移除问题。每个问题固定一个整数值函数 $f(n)$，其值仅对较小的 $n$ 已知，基准测试为其保留一个下界记录和一个上界记录。记录是一个可计算的 Lean 函数，并带有机器验证的证明，证明它界定了 $f$。提交者提出一个新函数，并证明它界定了 $f$，证明它在任何 $n$ 处都不比当前记录差，并且证明它在某个 $n$ 处严格更优。一旦被接受，它就成为下一次提交必须超越的记录。因此，该系统既选择界，也选择其证明，并且它可以在单个 $n$ 处或在其增长率上改进记录。在每个 $n$ 处，两个记录之间的差距显示了已认证的界距离确定 $f(n)$ 还有多远。每个证明都由两个独立的 Lean 内核检查，因此无需审稿人检查数学内容。这些检查还会拒绝通过在小 $n$ 处穷举搜索来计算 $f$ 的函数，而维护者只需阅读提交者的报告，并查找在更大 $n$ 处的此类搜索。我们发布了来自极值组合学的十个问题，包含二十个已证明的初始记录以及准入工具。作为基线，基于前沿语言模型的智能体，每个记录最多用一小时，有 82 份提交被接受，并改进了每一项记录，且未超出已发表的文献。基于两个更新模型的智能体随后从这些记录出发，又有 60 份提交被接受，并再次改进了 20 项记录中的 19 项。对于这十个问题中的八个，至少有一项记录在渐近意义上仍落后于已发表的最佳界。

提交历史

来自：Stefan Szeider [查看电子邮件]
[v1] 2026年10月9日星期五 11:59:46 UTC（32 KB）