AI benchmark tracks improving math problem solving limits
SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability
Artificial IntelligenceMachine LearningLogic in Computer Science
Summary
Measuring progress in AI math problem solving is difficult because benchmarks get too easy or problems only get solved once. The authors created SqueezeBench, a new way to evaluate progress continuously by raising the difficulty bar when a problem is solved better. This method uses computer-verified proofs to confirm improvements without needing human referees and prevents cheating by searching small cases exhaustively. The system was tested on ten hard math problems, with AI models consistently improving the records over time, but still leaving room for future advances.
What this means in practice
- •For ai developers: Use SqueezeBench to continuously test and improve AI models’ mathematical problem-solving abilities beyond fixed benchmarks.
- •For software verification teams: Employ computer-checked proofs to certify bounds and improvements in functions, enhancing confidence in automated reasoning tools.
Authors
Pablo Manrique, Hai Xia, Stefan Szeider
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.