arXiv cs.AI· Pablo Manrique, Hai Xia, Stefan Szeider·· 6 天前AI 评分36
SqueezeBench：抗饱和的数学能力评测基准
SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability
AI 导读
研究者提出 SqueezeBench，一种抗饱和的数学能力评测基准：每道题固定一个仅小 n 已知取值的整数函数 f(n)，提交需用 Lean 函数给出可机器验证的上下界证明，成功即抬高门槛而非移除题目。基准发布十个极值组合学问题与二十个已证初始记录；基于前沿语言模型的智能体在每题最多一小时限制下被接受 82 次提交并改进全部记录，两个更新模型的智能体又改进 20 个记录中的 19 个。
正文 · 原文
Abstract:AI systems are making rapid progress in mathematics, but this progress is hard to measure. Benchmarks of solved problems saturate, and in benchmarks of open problems each problem can be resolved for the first time only once. We present SqueezeBench, a benchmark that is resilient to saturation: a success raises the bar instead of removing the problem. Each problem fixes an integer function $f(n)$ whose values are known only for small $n$, and the benchmark keeps a lower and an upper record on it. A record is a computable Lean function with a machine-checked proof that it bounds $f$. A submission proposes a new function and proves that it bounds $f$, that it is no worse than the current record at any $n$, and that it is strictly better at some $n$. Once accepted, it becomes the record that the next submission has to beat. The system thus chooses the bound as well as its proof, and it may improve the record at a single $n$ or its growth rate. At every $n$, the gap between the two records shows how far the certified bounds are from determining $f(n)$. Every proof is checked by two independent Lean kernels, so no referee needs to check the mathematics. The checks also reject a function that computes $f$ by exhaustive search at small $n$, and a maintainer only reads the submitter's report and looks for such a search at larger $n$. We release ten problems from extremal combinatorics with twenty proved initial records and the admission tools. As a baseline, agents based on a frontier language model, with at most one hour per record, had 82 submissions accepted and improved every record, without going beyond the published literature. Agents based on two newer models then started from these records, had 60 more submissions accepted and improved 19 of the 20 records again. For eight of the ten problems, at least one record is still asymptotically behind the best published bound.
| Subjects: | Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2610.13461 [cs.AI] |
| (or arXiv:2610.13461v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.13461 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Stefan Szeider [view email]
[v1]
Fri, 9 Oct 2026 11:59:46 UTC (32 KB)
来源：arXiv cs.AI · arxiv.org