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

AI 系统在数学领域进展迅速，但这种进展难以衡量。由已解决问题构成的基准会趋于饱和，而在由未解决问题构成的基准中，每个问题只能被首次解决一次。我们提出了 SqueezeBench，这是一种抗饱和基准：一次成功会提高门槛，而不是移除问题。每个问题都固定一个整数函数 $f(n)$，其函数值仅在较小的 $n$ 上已知，基准则为该函数维护一项下界纪录和一项上界纪录。每项纪录都是一个可计算的 Lean 函数，并附有经机器检查的证明，证明它是 $f$ 的界。每次提交都提出一个新函数，并证明它是 $f$ 的界、在任意 $n$ 上都不劣于当前纪录，且在某个 $n$ 上严格优于当前纪录。一旦获准接受，它就成为下一次提交必须超越的纪录。因此，系统既要选择界，也要给出相应证明；它可以改进某个特定 $n$ 上的纪录，也可以改进其增长率。对于每个 $n$，两项纪录之间的差距表明，经认证的界距离确定 $f(n)$ 的值还有多远。每个证明都由两个独立的 Lean 内核检查，因此无需评审人员核查数学内容。这些检查还会拒绝在较小的 $n$ 上通过穷举搜索计算 $f$ 的函数，而维护者只需阅读提交者的报告，并检查在较大的 $n$ 上是否存在此类搜索。我们发布了极值组合学中的十个问题、二十项附有证明的初始纪录，以及提交准入工具。作为基线，基于一个前沿语言模型的智能体在每项纪录最多一小时的限制下，有 82 次提交获准接受，并改进了所有纪录，但未超越已发表文献中的结果。随后，基于两个更新模型的智能体从这些纪录出发，又有 60 次提交获准接受，并再次改进了 20 项纪录中的 19 项。在十个问题中的八个上，仍有至少一项纪录在渐近意义上落后于已发表的最优界。