AI Puzzles: A New Paradigm Between Benchmarks and Open Problems

When Benchmarks Saturate and Competition Problems Get Memorized, How Do We Measure AI's True Reasoning Ability?

Current AI evaluation systems face an awkward three-way dilemma: benchmark questions are fixed with hidden answers, but once models max out the leaderboard, they lose discriminative power. Competition problems, while solved, are easily memorized by models. And open-problem lists lack clear evidence and success criteria, making it hard to judge whether AI has truly advanced understanding. A new format recently discussed in the Reddit community—AI puzzles—attempts to find a balance point among these three.

This concept was proposed by researcher Jarek Duda, using the field of aperiodic order as a pilot, constructing a tiered ladder-style puzzle set. Its core design philosophy: arrange problems from the same research field by difficulty from "human level" (solvable with pen and paper) to "ASI level" (completely open), with each level genuinely harder than the last.

How the Puzzle Ladder Works: Verifiability Is Key

The most noteworthy design of this format lies in its strict definition of what counts as "solved."

Solved Levels: Training and Verification

Lower-level puzzles in the ladder have precise answers that can be automatically verified by programs. This means they can be used both for training models and for checking model outputs—and questions can easily be varied to prevent models from cheating through answer memorization.

Benchmark saturation refers to when a model's score on a benchmark approaches or reaches the ceiling, causing that benchmark to no longer distinguish capability differences between models. This phenomenon stems from fixed questions and answers in benchmarks, allowing models to "game the leaderboard" through large-scale training or targeted optimization rather than genuinely improving reasoning. For example, many commonsense reasoning benchmarks saturated rapidly after the emergence of large language models, forcing researchers to constantly design harder new benchmarks. Saturation not only wastes evaluation resources but can also lead to misjudgments of model capabilities—high scores may reflect memorization or overfitting rather than generalized reasoning. AI puzzles circumvent saturation through open levels and dynamic variants, because open problems have no fixed answers and models cannot reach a ceiling by grinding through problems.

Open Levels: Everything Solvers Need

Higher-level open puzzles provide all materials needed for solving: strong numerical evidence, known failed paths, relevant files, and a machine-checkable success criterion. There is an iron rule here: only checkable proofs count; floating-point values are merely evidence, not proof. This distinction strikes directly at the pain point of current AI reasoning evaluation—models frequently package numerical estimates as "proofs" while lacking formal verification.

Additionally, solvers of open levels are credited by name, including the agents and models used, recorded in the next version of the paper. This provides a traceable contribution attribution mechanism for AI-assisted research.

Formal verification refers to using mathematical logic and computer programs to rigorously prove the correctness of a proposition, with the core being the transformation of proofs into machine-checkable steps. Unlike numerical estimates, formal proofs do not rely on approximation or probability but provide absolute certainty. In AI reasoning evaluation, formal verification can effectively distinguish "guessing" from "proving": models can generate numerical results, but only proofs that pass formal checks truly count as solving a problem. Common tools include interactive theorem provers (such as Coq, Lean) and automated theorem provers. AI puzzles emphasize that only machine-checkable proofs count, precisely to push AI from generating plausible-looking answers toward producing rigorously verifiable reasoning chains.

First Real-World Test: Grok's "Stumble" and Correction

This puzzle format has already undergone a public first test. According to the Reddit post, when Grok was publicly asked an open-level puzzle, it claimed to provide a proof but actually only gave a numerical estimate, then retracted the claim.

More intriguing is its performance at other levels: it initially answered incorrectly at the human level, corrected after one hint; and passed the expert level on the first try. This "uneven" performance pattern precisely exposes the instability of current models in distinguishing "guessing" from "proving"—it can solve certain expert-level problems yet make mistakes at basic levels, and easily mistakes estimates for proofs.

That said, on MathOverflow, experts are already testing the highest-level constructions. This shows the format is not only aimed at AI but also attracting human researchers.

Aperiodic order is a concept in mathematics and physics describing an ordered structure that is neither fully periodic nor completely random. The most famous example is Penrose tiling, which uses two types of rhombi to tile the plane in a non-repeating way while possessing long-range order. Aperiodic order has applications in quasicrystals, number theory, and dynamical systems, with research involving complex combinatorial and geometric problems. Jarek Duda likely chose this field as the pilot for AI puzzles because it has both precise formal definitions and numerous open problems, some of which can be transformed into computationally verifiable forms. The ladder-style puzzle design in aperiodic order provides a reference template for formalizing open problems in other fields.

Why This Format Deserves Researchers' Attention

From a methodological perspective, the value of AI puzzles lies in transforming "the frontier of a field" into a form that both AI agents and humans can practically attack. For researchers, this is a standardized interface for handing their open problems to AI for attempts; for evaluators, it provides an observation window: can models distinguish guessing from proving?

Compared to traditional benchmarks, its advantage is saturation resistance—because open levels have no fixed answers, models cannot saturate through grinding. Compared to open-problem lists, its advantage is having clear success criteria—machine-checkable proofs.

However, this format is currently piloted only in the single research field of aperiodic order, with the dataset published on HuggingFace, and the highest-level puzzles publicly discussed on MathOverflow. Whether it can be generalized to other disciplines depends on whether each field can formalize its own open problems into "machine-verifiable ladders."

Challenges of Generalization and Open Discussion

The question posed at the end of the post is: Would you use this format in your own field to organize open problems?

Several practical challenges lie behind this. First, "proofs" in many fields are difficult to machine-verify, and success criteria in non-formalized fields are hard to unify. Second, designing tiered ladders requires significant effort from domain experts to decompose problems into sequences of increasing difficulty. Third, how to define attribution mechanisms and contribution recognition when AI participates in research remains an open question.

But the direction is clear: as benchmarks continue to saturate and competition problems become contaminated by memorization, AI evaluation needs more intermediate forms like AI puzzles that are "both open and verifiable." It does not seek to provide ultimate answers in one shot but constructs a climbable ladder from the known to the unknown—perhaps closer to the true form of scientific research than any single leaderboard.

One-line Summary

AI puzzles: between benchmarks and open problems, measuring AI reasoning through verifiable proofs.

Paragraph Summary

Current AI evaluation faces a triple dilemma: benchmark saturation, competition problems being memorized, and open problems lacking standards. Researcher Jarek Duda proposed the "AI puzzles" format, piloted in the aperiodic order field, grading problems by difficulty from human level to ASI level to form a ladder. Its core rule is that only machine-checkable proofs count as solved, with floating-point values being merely evidence. In the first test, Grok mistakenly reported numerical estimates as proofs on an open puzzle and retracted, exposing model instability in distinguishing guessing from proving. The format resists saturation through open levels and dynamic variants, and provides attribution tracing for AI-assisted research. Though generalization faces challenges such as the difficulty of formalizing fields, the direction is clear: building an intermediate form that is both open and verifiable, closer to the true form of scientific research.