SqueezeBench
A saturation-resistant benchmark for evaluating AI mathematical capabilities. It replaces fixed-answer problems with integer function boundaries that continuously tighten, and uses the Lean theorem prover for machine verification, allowing the benchmark to evolve alongside model capability improvements without losing discriminative power.
Timeline (last 90 days)
SqueezeBench is a saturation-resilient AI mathematics evaluation benchmark whose core mechanism is that solving a problem does not remove it but instead raises its threshold.
Each problem in SqueezeBench corresponds to an integer function f(n), and the benchmark maintains a lower-bound record and an upper-bound record for each function.
A record in SqueezeBench refers to a computable Lean function accompanied by a machine-verifiable proof.
When submitting new results, one must prove that the new function genuinely bounds f, is no worse than the current record at any n, and is strictly better than the current record at at least one n.
Every proof in SqueezeBench is checked by two independent Lean kernels, and the entire mathematical correctness review requires no human referee.
The SqueezeBench system actively rejects functions that compute f by exhaustive search over small values of n, in order to guard against cheating through memorization rather than genuine mathematical reasoning.
The research team released ten problems from the field of extremal combinatorics, along with twenty proven initial records and admission tools.
An agent based on a certain frontier language model, under a limit of at most one hour per record, had 82 submissions accepted and improved all records, but the improvements did not go beyond the scope of published literature.
Agents based on two newer models continued from these records, with 60 more submissions accepted, further improving 19 out of 20 records.
For eight of the ten problems, at least one record still asymptotically lags behind the best bounds published in the literature.
3 more timeline events
All Facts (13)
SqueezeBench is a saturation-resilient AI mathematics evaluation benchmark whose core mechanism is that solving a problem does not remove it but instead raises its threshold.
50%UnverifiedEach problem in SqueezeBench corresponds to an integer function f(n), and the benchmark maintains a lower-bound record and an upper-bound record for each function.
50%UnverifiedA record in SqueezeBench refers to a computable Lean function accompanied by a machine-verifiable proof.
50%UnverifiedWhen submitting new results, one must prove that the new function genuinely bounds f, is no worse than the current record at any n, and is strictly better than the current record at at least one n.
50%UnverifiedEvery proof in SqueezeBench is checked by two independent Lean kernels, and the entire mathematical correctness review requires no human referee.
50%UnverifiedThe SqueezeBench system actively rejects functions that compute f by exhaustive search over small values of n, in order to guard against cheating through memorization rather than genuine mathematical reasoning.
50%UnverifiedThe research team released ten problems from the field of extremal combinatorics, along with twenty proven initial records and admission tools.
50%UnverifiedAn agent based on a certain frontier language model, under a limit of at most one hour per record, had 82 submissions accepted and improved all records, but the improvements did not go beyond the scope of published literature.
50%UnverifiedAgents based on two newer models continued from these records, with 60 more submissions accepted, further improving 19 out of 20 records.
50%UnverifiedFor eight of the ten problems, at least one record still asymptotically lags behind the best bounds published in the literature.
50%UnverifiedUnder strict machine-verification standards, the currently strongest AI agents have not yet been able to match the best results achieved by the human mathematics community in the field of extremal combinatorics.
50%UnverifiedThe upper and lower bounds for extremal combinatorics problems often come from different proof techniques, and there is frequently an asymptotic gap between them that is difficult to close, making them naturally suited to the SqueezeBench framework of maintaining upper and lower bounds and continuously tightening them.
50%UnverifiedCross-validation by two independently implemented Lean kernels is an additional defensive measure; if both accept the same proof, the probability of a common error is extremely low.
50%