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

arXiv:2610.13461v1 公告类型：cross 摘要：AI 系统正在数学领域取得快速进展，但这种进展很难衡量。已解决问题的基准会趋于饱和，而在开放问题基准中，每个问题只能被首次解决一次。我们提出了 SqueezeBench，这是一种抗饱和基准：一次成功会提高标准，而不是移除问题。每个问题确定一个整数函数 $f(n)$，其取值仅在较小的 $n$ 上已知，基准则持续维护该函数的下界记录和上界记录。记录是一个可计算的 Lean 函数，并附有机器检查的证明，证明其确实界定了 $f$。提交内容需要提出一个新函数，并证明它界定了 $f$、对任意 $n$ 都不劣于当前记录，且在某个 $n$ 上严格更优。一旦被接受，它就会成为下一份提交必须超越的记录。因此，该系统不仅选择界，还选择其证明；它既可能在某个单独的 $n$ 上改进记录，也可能改进其增长率。在每个 $n$ 上，两条记录之间的差距表明，经认证的界距离确定 $f(n)$ 还有多远。每个证明都由两个相互独立的 Lean 内核检查，因此无需裁判检查数学内容。这些检查还会拒绝一种通过在较小 $n$ 上穷举搜索来计算 $f$ 的函数，而维护者只需阅读提交者的报告，并检查其是否在更大的 $n$ 上进行此类搜索。我们发布了十个来自极值组合学的问题、二十条已证明的初始记录以及准入工具。作为基线，基于前沿语言模型的智能体在每条记录最多使用一小时的情况下，有 82 份提交被接受，并改进了每一条记录，且没有超出已发表文献的范围。随后，基于另外两个更新模型的智能体从这些记录出发，又有 60 份提交被接受，并再次改进了 20 条记录中的 19 条。对于十个问题中的八个，至少有一条记录在渐近意义上仍落后于已发表的最佳界。