SqueezeBench: The Shooting Target That Keeps Growing
*"The vitality of benchmarks" series, Part 1: the target runs on its own — when AI succeeds, SqueezeBench doesn't lose a problem; it gains a harder one.*
> One-line summary: Researchers at TU Wien (Pablo Manrique, Hai Xia, Stefan Szeider) built a benchmark that cannot die: SqueezeBench only includes combinatorics problems whose answers are known to exist but whose exact values humans don't know, and it turns "answering" into "record-breaking" — every AI-submitted tighter bound immediately becomes the next threshold everyone must surpass. Success doesn't exhaust it; success feeds it.
When Every Examinee Scores Full Marks
Traditional AI benchmarks are shooting ranges: targets hang on the wall, each bullet hits or misses, and the total score is the model's report card. The quiet assumption: the targets never move.
That assumption broke the day models started scoring full marks. A benchmark is just a stack of questions with standard answers — and once training data covers the stack, rising scores no longer mean rising capability. Worse, the arms race is asymmetric: a human team spends months crafting hard problems; a model solves them in one afternoon of inference. miniF2F gave way to PutnamBench; PutnamBench to FrontierMath. But swapping exams just installs a new ceiling that will eventually be punched through.
Could a benchmark be built that never becomes obsolete? The paper's answer rests on a simple observation: in mathematics, there is a class of problems where the target itself is alive.
The Perfect Continent: The Answer Exists, the Value Is Unknown
Extremal combinatorics studies discrete structures — points, lines, sets, graphs — and asks blunt questions: how much can you pack in? How small can it be? Examples featured in SqueezeBench:
- Diagonal Ramsey numbers R(n,n): the minimum party size guaranteeing n mutual acquaintances or n mutual strangers. For n=5, the answer is known to lie between 43 and 48 — but nobody knows which integer.
- Golomb rulers: rulers whose marks have all pairwise distances distinct. With 4 marks, exhaustive search shows the shortest ruler is 6 units (marks at 0, 1, 4, 6). For 28 marks, humanity only knows: 536 ≤ f(28) ≤ 585.
- Cap sets in F₃ⁿ: the maximum number of pieces placed in an n-dimensional grid over {0,1,2} with no three collinear.
- Lower-bound record l(n): a certified function claiming "f(n) is at least me"
- Upper-bound record u(n): a certified function claiming "f(n) is at most me"
- Pre-check: submissions may only modify files inside the new-record directory; the core definition file
Def.leanmust be ≤ 64KiB and contain only pure definitions (Gates 1–2). - Gate 3: the Comparator tool (from Lean FRO) runs the proof through two independently developed kernels — the Lean kernel and nanoda — and only three whitelisted axioms are allowed (
propext,Quot.sound,Classical.choice). - Gate 4: compute budget is hard-capped — no brute-forcing around the clock.
- Gate 5: the new record must be a computable function that does not reference the conjectured f itself.
- Gate 6: the kernel actually evaluates the function at n = 1 to 100, catching any lookup-table cheating on small cases.
- 82 submissions accepted in the baseline stage; 60 more accepted in stage 2.
- 19 of 20 records improved.
- Yet on 8 of 10 problems, at least one record still trails the best human-published bound.
- Manrique, P., Xia, H., & Szeider, S. *Saturation-Resilient Evaluation of Mathematical Capability*. arXiv:2610.13461.
- Paper: https://arxiv.org/abs/2610.13461
These problems share three properties that make them ideal:
1. The answer is a concrete integer that stands there waiting. 2. Small cases are computable by exhaustive search — the function is "solid" at the start. 3. No formula exists for the middle and far range — human knowledge is a pipe: solid at both ends, hollow in between.
Because the standard answers don't even exist yet, memorization is useless: what would you memorize?
Changing the Question: Not "What Is It?" but "How Close Are You?"
Traditional benchmarks ask "what is the value?" — right or wrong, and the question dies. SqueezeBench asks: "How far can you close the gap?"
Each problem is defined by two record lines:
The true f(n) is squeezed between them, and the gap u(n) − l(n) is humanity's current "width of ignorance." Every accepted record automatically raises the bar — the competition can go on forever.
The Vise: Valid, Improves, Strict
A new lower-bound l′(n) must come with three machine-checkable proofs:
1. Valid: l′(n) ≤ f(n) everywhere — the claim really is a lower bound. 2. Improves: l(n) ≤ l′(n) everywhere — no regression anywhere. 3. Strict: there exists at least one n₀ where l(n₀) < l′(n₀) — a genuine advance somewhere.
The upper bound works symmetrically. The unit of a record is a function, not a scalar: improvements can be local and incremental ("I cracked n=37") without needing to be uniformly better. When u(n) and l(n) finally meet, the problem is solved — the benchmark's terminal fate is to have truth abolish it.
Six Security Gates: Machines Verify Everything
All verification is automated, built on Lean 4:
All six gates block the same core cheat: fabricating an exact value you could never compute. Once accepted, a record carries lifetime endorsement from two independent kernel auditors — no human mathematician ever reads the proof.
Experiments: How Much Ground Did Frontier Models Cover?
Setup: 10 extremal combinatorics problems, 20 certified initial records (an upper and lower bound each). Stage 1: Claude Code agents (Opus 5), 1-hour budget per problem, warming up the field. Stage 2: Fable 5.1 agents handled 19 of the 20 records; an Opus 5.5 agent tackled the Golomb ruler lower bound; both could consult a GPT-6 Astra API. Each run: up to ~2 hours, 32 GiB memory, stop notices at 80 minutes or 55% context use.
Results:
That last number says three things at once: the AI submissions are not parroting the literature (otherwise the "trailing" rate would be near zero); current agent configurations remain visibly short of decades-old human frontiers; and every millimeter of progress in the repository is machine-verified — this benchmark doesn't inflate. And when the final submission was accepted, every record line stood higher than before: the benchmark got harder.
One Exam, Three Fates
| | Traditional math benchmarks (miniF2F, PutnamBench) | Open-problem archives (Ramsey, Cages) | SqueezeBench | |---|---|---|---| | Record-type functions, replaceable | ❌ | ✅ | ✅ | | Must prove "no worse than incumbent" | – | ❌ | ✅ | | Two-sided upper/lower squeezing | ❌ | Partial | ✅ | | Automatic proof verification | ❌ | ❌ | ✅ | | Humans and AI submit alike | – | Humans only | ✅ |
Traditional benchmarks are closed-book exams that die on saturation. Open-problem archives are hand-written Guinness records maintained by human communities. SqueezeBench fuses the two: certification rigor is delegated to machines, participation is open to everyone. Its leaderboard is not a snapshot but a chronicle: every record carries a date, author, and witness point n₀, fully traceable — invaluable for studying AI capability over time.
The Privilege of Mathematics: A Vault That Only Grows
The mechanism would fail in most fields, but mathematics has a nearly unique privilege: a proven theorem stays proven forever. Certified records never expire, so the repository only grows — every AI success is forged into a rust-free stepping stone for the next challenger. There is also a cultural irony: formalization was developed to stop humans from erring; in the AI era it has become the neutral referee for human–machine fair competition.
Back to Galileo: his greatness was not measuring one number, but inventing a method of measurement that can be refined indefinitely — every generation makes the incline flatter and the water clock more precise. SqueezeBench does the same for evaluation: any future model, three months or three years out, can stand on the current records and push further. Its "immortality" is directional — each squeeze both raises the bar and brings humanity one inch closer to the sleeping integer. Its ultimate fate is to be abolished by truth itself.
It is not a panacea: it requires problems whose answers are objective integers, which is why the raw material is extremal combinatorics rather than the Riemann Hypothesis. Building similarly "growing" benchmarks for fuzzier domains — physics, coding, writing — is the genuinely hard question this paper leaves the evaluation community.
Key Numbers
| Item | Value | |---|---| | Problems included | 10 (all extremal combinatorics) | | Initial records | 20 (upper + lower bound each) | | Submissions accepted, baseline stage | 82 | | Submissions accepted, new-model stage | 60 | | Records improved by new models | 19 / 20 | | Problems still trailing literature | 8 / 10 | | Verification gates | 6 | | Independent Lean kernels | 2 (Lean kernel + nanoda) | | Def.lean size cap | ≤ 64KiB | | Kernel evaluation points | n = 1 to 100 | | Per-run limits | ~2 hours / 32GiB RAM | | Stop-notice timing | 80 min or 55% context | | Golomb ruler example | 536 ≤ f(28) ≤ 585 |