Source-linked AI summary
SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability
Pablo Manrique, Hai Xia, Stefan Szeider
TL;DR
Solved-problem benchmarks can saturate, while open-problem benchmarks offer each problem only one first resolution. SqueezeBench tracks machine-checked lower and upper function bounds that submissions must improve; agents improved most records, though many remain behind published bounds.
Problem
Solved-problem benchmarks can saturate, while each open problem yields at most one first resolution and intermediate progress such as a better bound earns little or no credit.
Source: §1 · pp. 1–2Method
SqueezeBench stores machine-proved lower and upper bounds as computable Lean functions and accepts a replacement only when it is valid, no worse at any n, and strictly better somewhere.
Source: §1 · p. 2Results
After 82 accepted baseline submissions improved every record, newer-model agents had 60 more accepted and improved 19 of 20 records again; eight of ten problems still have a record asymptotically behind the best published bound.
Source: §1 · p. 3, §6 · p. 10Takeaways & Limitations
At each n, the gap between the lower and upper records shows how far the certified bounds remain from determining f(n).
Source: §1 · p. 2The ten problems cover one area of mathematics and one parameter each, and the model runs were not controlled comparisons from a shared snapshot with equal budgets.
Source: §6 · p. 10
Abstract
from arXiv · showhide
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.
1 Introduction
SqueezeBench addresses saturation and one-shot resolution in existing mathematics benchmarks by tracking machine-proved lower and upper function bounds that submissions must improve. It combines mechanically checked admission with agent evaluations across ten extremal-combinatorics problems.
1 Introduction
- Solved-problem benchmarks can saturate, while open-problem benchmarks yield at most one first resolution and give little credit for intermediate progress such as a better bound.Existing record archives keep improvable records, but use fixed-problem numbers checked by witnesses or citations rather than kernel-checked proofs of bounds.Source: §1 · pp. 1–2
- SqueezeBench keeps lower and upper computable-function records, replaced only by a proved bound that is no worse everywhere and strictly better somewhere.An accepted record raises the bar for the next submission, while the gap between records at each n indicates how far the bounds are from determining f(n).Source: §1 · pp. 2–3
- Systems start from the same record snapshot and budget, and their reached bounds are compared value by value rather than by submission count.Initial records are weaker than published bounds, so early literature-based improvements are reported as a catch-up phase.Source: §1 · p. 2
- Two independent Lean kernels check proofs against statements fixed in advance, while mechanical checks and a maintainer review address exhaustive search and formalization fidelity.New records are evaluated at every n ≤ 100 within a fixed budget; a maintainer also reads reports for searches above that threshold and checks each formal definition against its intended question once per problem.Source: §1 · pp. 2–3
- The baseline accepted 82 submissions and improved every record; the continuation accepted 60 more and improved 19 of 20 again, while eight problems retain a record asymptotically behind literature.The number of records matching the leading term of the best published bound rose from four to ten.Source: §1 · pp. 2–3
- The release includes ten extremal-combinatorics problems with proved initial lower and upper records, alongside admission tools and an evaluation harness.The evaluation covers three frontier-model agents on all twenty records, using an initial-record baseline and a continuation from the baseline records.Source: §1 · p. 3
2 Framework
SqueezeBench tracks proved lower and upper bounds on combinatorial functions whose exact values are known only for small parameters. Submissions propose computable Lean bounds that improve the current record without regressing, and are admitted through automated checks and maintainer review.
Problems
- Problems use a function f defined by its combinatorial meaning, typically as a finite maximum or minimum, with exact values known only for a small number of parameters.Bounds must be explicit and computable at every parameter, a stronger requirement than many asymptotic literature bounds with unspecified constants or restricted validity.Source: §2 · pp. 3–4
Bounds and records
- A record is a computable function bounding f at every n; a submission proves validity, no regression against the incumbent, and strict improvement at some n.The gap between upper and lower records measures how far the bounds are from determining f(n); for Golomb rulers, 536 ≤ f(28) ≤ 585.Source: §2 · p. 4
Challenges and submissions
- Submissions fill a trusted challenge’s open Lean definitions and proofs; Comparator checks the stated theorems and allowed axioms with the Lean kernel and an independent kernel implementation.The submission separates the new definition from proofs so later challenges can import the definition while keeping trusted files small.Source: §2 · pp. 4–5
Verification and acceptance
- Six verification gates constrain files, proof computation, computability, and record evaluation through n = 100; maintainers also inspect reports for searches above that threshold.The evaluation gate rejects exhaustive computation of f at small n, while the maintainer review checks for a search starting above n = 100.Source: §2 · p. 5
3 Related Work
SqueezeBench sits between mathematical reasoning benchmarks, theorem-proving tasks, and archives of best-known results. It maintains function-valued lower and upper records that submissions can improve without regression, addressing limits of solved-problem and open-problem benchmarks.
Benchmarks of solved and open problems
- Solved-problem benchmarks can saturate and expose public answers, while open-problem benchmarks lose informative tasks after first resolution and give little credit for intermediate bound improvements.A single proof of a conjecture may also fail to credit earlier work on which it builds.Source: §3 · p. 6
Archives and construction search
- Archives track moving best-known results, while newer collections accept claims backed by citations or update tasks semi-automatically; SqueezeBench instead requires a Lean proof valid at every n.Fun-Search, AlphaEvolve, and PatternBoost find constructions by search and check them with a program; those systems can supply constructions for Lean proof.Source: §3 · p. 6
Comparison with benchmarks and archives
- Only SqueezeBench among the compared systems replaces function-valued records while proving that replacements never regress.Table 1 compares mathematical benchmarks and record archives across target type, two-sided bounds, checking method, and other properties.Source: §3 · p. 6, Table 1 · p. 7
4 Problems
SqueezeBench includes ten formalized extremal-combinatorics problems and can add further qualifying problems. Its Golomb-ruler example shows how a combinatorial optimum becomes a Lean function and how explicit constructions support bounds.
4 Problems
- The problem list is open to additions that meet the benchmark’s requirements, with proposals welcomed from the community.The ten problems span additive combinatorics, extremal graph theory, and Ramsey theory.Source: §4 · p. 7, §4.1 · p. 7
4.1 The ten problems
- The ten problems have one integer parameter and exact values known only at small sizes, including n ≤ 4 for R(n, n) and n ≤ 28 for Golomb rulers.Table 2 presents their standing records after the experiments and marks matches to published bounds or elementary bounds.Source: §4.1 · p. 7, Table 2 · p. 8
4.2 Running example: Golomb rulers
- For Golomb rulers, f is the minimum ruler length for a given number of marks, formalized through finite Sidon sets whose pair sums determine the same pair.The binary ruler is proved to satisfy the ruler condition so that a lower bound on f can be established.Source: §4.2 · p. 8
5 Evaluation
The evaluation ran two agent phases on ten problems, with the second phase starting from the first phase’s records. Both phases improved records, though several remain behind published bounds.
Evaluation protocol
- The first phase used Opus 5 from elementary seeds for up to an hour; the second launched Fable 5.1 on 19 records and Opus 5.5 on the Golomb-ruler lower record, with possible GPT-6 Astra consultation.The second-phase runs took up to about two hours, and prompts and outside-source rules changed during the runs.Source: §5 · p. 9
- Agents worked one per track, reading the problem and current records, then proving validity, improvement, and strict improvement before verifying and accepting each new record.Every second-phase record was independently re-verified before merging, and both phases were later audited.Source: §5 · p. 9
Results
- 82 submissions were accepted in 18.9 hours in phase one; phase two accepted 60 more and improved 19 of 20 records again, while eight problems still have a record behind published bounds.Every one of the twenty records improved on its seed.Source: §5 · pp. 9–10
- f(50) ≤140 and f(100) ≤529, versus literature-derived bounds of 144 and 566, for the Ruzsa–Szemerédi upper record.The paper reports no published bound giving these values, though the record remains asymptotically behind the o(n^2) triangle-removal-lemma bound.Source: §5 · pp. 9–10
Running example
- On Golomb rulers, Fable 5.1 lowered the upper record from 1,570 to 585 at n=28 and from 20,002 to 8,831 at n=100.Opus 5 reached about 2n^2, while Fable 5.1 brought in constructions of about n^2; the records determine f(n) for n ≤5 and leave gaps of 49 at n=28 and 621 at n=100.Source: §5 · p. 10
Results
- For C4-free graphs and Golomb rulers, both records match the leading term of the best published bounds; the other eight problems have at least one record behind.Some published bounds are unformalized or have constants too weak at these values, and exhaustive-search impossibility results lack short certificates within the computation budget.Source: §5 · p. 10
6 Conclusions
SqueezeBench tracks mathematical progress through certified, improvable bounds rather than solved statements. In the evaluation, later agents improved most records again, while the benchmark remains limited in scope and comparison conditions.
Conclusion
- A submission replaces a record only by proving it valid, no worse at any n, and better at some n, with checks by two kernels against fixed statements.The record history is the leaderboard.Source: §6 · p. 10
- After baseline agents made 82 accepted submissions, newer-model agents made 60 more and improved 19 of 20 records again; eight of ten problems still have a record behind the literature.Source: §6 · p. 10
Limitations
- The benchmark has ten problems from one area with one parameter each, and the runs were not equal-budget comparisons from a shared snapshot.A maintainer still checks reports for searches above n=100, and bounds known only from exhaustive computer searches cannot enter within the budget.Source: §6 · p. 10
Use of AI assistants
The authors used AI tools in benchmark development, literature work, and manuscript preparation, and reviewed the assisted work.
Use of AI assistants
- AI tools helped implement benchmark tools and Lean formalizations, develop admission checks, compare records with literature, and draft text and figures; the authors reviewed the assisted work and take responsibility for the final content.Source: Use of AI assistants · p. 11
A Adding a problem
Adding a problem requires defining its combinatorial function, seeding both bound records, configuring and testing admission checks, and documenting and reviewing the problem. A tutorial problem provides a place to practice the submission workflow.
Adding a problem
- Define nmin and f by the problem’s combinatorial meaning, reduce each bound to its combinatorial content, and check evaluable small values by decide.For a least-element function, prove the defining set is nonempty so a lower record can be proved.Source: A Adding a problem · p. 14
- Seed both directions with V000 records that are simple to formalize and not taken from known values.Each seed includes a record definition, validity proof, metadata, and report.Source: A Adding a problem · p. 15
- Configure nmin, directions, gate-6 budget, oracles, and forbidden constants, then generate and audit the first challenges for each direction.The audit checks that seeds pass their own challenges with only the three standard axioms.Source: A Adding a problem · p. 15
- Document the statement, known values, sources, and literature; a maintainer checks that f denotes the intended object before admitting the problem.The accepted problem then appears in squeeze like the others.Source: A Adding a problem · p. 15
Tutorial
- A separate tutorial problem—the largest subset of {1, ..., m} containing no element together with its double—lets newcomers check f by decide and practice submissions.Source: A Adding a problem · p. 15