FormulaOne

FormulaOne is an AI benchmark for evaluating whether a model can design and implement dynamic programming algorithms for graph problems. Gal Beniamini and 12 coauthors introduced it in an arXiv preprint submitted on July 17, 2025. The paper defines a 120-problem core benchmark and a separate 100-problem FormulaOne-Warmup set. Both use properties expressible in monadic second-order logic and provide a tree decomposition with each input graph.^[1]

The benchmark isolates a specific form of algorithmic reasoning. A system does not have to parse the graph format, construct a tree decomposition, or write an entire program. It must define the state and transitions for a supplied evaluation framework and return an exact weighted count. The authors' July 2025 evaluation reported that o3, o3-Pro, and Gemini 2.5 Pro each solved one of the 120 core problems, while Grok 4 Heavy solved none.^[1] These are benchmark-author results under different numbers of attempts, not an independently reproduced or current leaderboard comparison.

Dataset scope and naming

The paper and the public repository distinguish two datasets. FormulaOne is the 120-problem core, and FormulaOne-Warmup is an auxiliary set of 100 easier problems. The repository contains 120 core JSON records and 100 Warmup records, together with evaluation code, the evaluation prompt, and a human-written Dominating Set example. Its release commit is dated August 14, 2025.^[2][3]

The current official project page presents the same 220 problems as one suite with three difficulty tiers. In that presentation, the 100 Warmup problems are the Shallow tier, while the original 120-problem core is divided into 100 Deeper and 20 Deepest problems.^[4] Keeping the two naming systems separate avoids the mistaken claims that the original paper defined a 220-problem core or that Warmup is an additional set beyond the 220 tasks.

Scroll sideways for more →

The repository publishes complete tests for Warmup. For the 120 core tasks, it publishes the problem statements and only a subset of the full tests; the remaining tests are withheld for submitted evaluations. The repository licenses its evaluation code under Apache 2.0 and the public problem statements and input-output material under CC BY 4.0.^[2] A result obtained only on the public core subset is therefore not equivalent to a result on the private benchmark suite.

Task formulation

Each task supplies an undirected graph, a tree decomposition, and integer weights on either the vertices or the edges. Its logical condition is a unary open formula: the free variable represents a candidate vertex set or edge set. The requested output is a weighted model count. For every satisfying set, the weights of its elements are summed, and those sums are then added across all satisfying sets. The final value is reported modulo 1,000,000,007.^[1]

Most formulas in the release belong to MSO1, the form of monadic second-order logic that quantifies over vertices and vertex sets. The paper notes that the broader framework could also express other objectives or use richer logics, but the released tasks use weighted model counting and allow a single post-order traversal of the supplied tree decomposition. Claims about optimization objectives, multiple traversal passes, or an unlimited generated corpus describe proposed extensions, not content already present in the release.^[1]

The theoretical motivation comes from Courcelle's theorem. For a fixed monadic second-order formula and a fixed bound on treewidth, the relevant graph property can be decided in time linear in the graph size, with potentially large dependence on the formula and treewidth.^[5] This is an existence and tractability result. It does not directly provide the compact state representation or practical transitions required by a FormulaOne submission.

The evaluation framework converts the supplied decomposition into a nice tree decomposition and traverses it. A submission implements five Python functions: callbacks for leaf, introduce, forget, and join nodes, plus a function that extracts the answer from the root table. Each callback sees only the subgraph induced by the vertices in its current bag.^[1][6] This design removes input handling and decomposition construction from the evaluated work, concentrating the task on state design, transition logic, counting, and implementation.

Problem generation and testing

The paper describes a domain-specific language that produces a human-readable task, a verifier, test instances, and a specification of a valid dynamic programming state. That specification is used to estimate complexity and set tractable tests. The authors report allowing time limits up to 100 times the expected running time of the annotated solution so that evaluation is less sensitive to modest implementation overhead.^[1]

Test graphs and tree decompositions are sampled through Markov chains intended to vary low-treewidth graph structure while controlling treewidth. The evaluation uses four kinds of tests:^[1]

• Correctness tests compare a candidate with brute-force answers on small graphs.
• Consistency tests run the same graph and weights with perturbed tree decompositions, because the mathematical answer must not depend on the chosen decomposition.
• Efficiency tests increase graph size or use extremal structures to expose implementations that do not meet the required fixed-parameter linear behavior.
• Sporadic or exotic tests use selected graph families intended to cover unusual local structures.

The paper states that the sampling method covers small graph gadgets with high probability. That is a property claimed for the generator, not a formal guarantee that a finite hidden suite detects every incorrect program. As with other test-based coding benchmarks, passing indicates success on the evaluator's cases rather than a proof of correctness for every possible graph.

Original model evaluation

The paper evaluated four reasoning models with their highest available reasoning setting and maximum reasoning and output token allowances. Its prompt supplied the framework instructions, utility definitions, and three worked examples.^[1][7] The framework then extracted the five required functions from each completion and ran them against the benchmark tests.

The reported results were:^[1]

Scroll sideways for more →

Success at k meant that at least one of k attempts passed. The paper used 10 independent completions for o3 and Gemini 2.5 Pro, but one completion for o3-Pro and Grok 4 Heavy. The authors wrote that the latter two systems already aggregated multiple samples internally. They also disclosed that Grok 4 Heavy had internet access while the other models did not, because of technical constraints.^[1] The table therefore supports the stated per-model benchmark outcomes, but the products' different aggregation methods do not provide a directly comparable per-completion accuracy measure.

The results are also time-bounded. They describe model versions and settings evaluated by the benchmark authors in July 2025. The public leaderboard application's source labels its landing-page accuracy data as static and not tied to leaderboard submissions.^[8] Those display values should not be substituted for verified submitted results. A later claim about a model, a tier, or a leaderboard position needs the model version, attempt policy, test regime, and evaluation date.

Interpretation and limitations

FormulaOne differs from ordinary competitive programming because it fixes a narrow mathematical family and removes much of the surrounding software work. The main challenge is to derive a correct bounded-treewidth state and all of its transitions. By contrast, benchmarks such as LiveCodeBench use contest problems across broader algorithmic topics and organize evaluation by release date to reduce contamination.^[9] OpenAI separately reported that an early o3 system reached an elite Codeforces rating and an International Olympiad in Informatics gold-medal level under its evaluation conditions.^[10] Those results establish strong performance on a different task distribution; they do not by themselves predict FormulaOne performance.

The FormulaOne authors call the domain "in-distribution" because graph algorithms, dynamic programming, and formal logic are represented in technical literature and model training data.^[1] The paper does not audit the evaluated models' private training corpora, however. "In-distribution" is therefore the authors' characterization of the subject area, not a measured property of each model's training set.

The benchmark also has a restricted scope. It evaluates Python callback synthesis for weighted model counting on supplied decompositions. It does not directly measure construction of tree decompositions, unrestricted graph algorithms, general software engineering, theorem proving, or all forms of mathematical reasoning. Its exact evaluator is a strength for reproducibility, but the private core tests mean that the complete core evaluation cannot be rerun locally from the public repository alone.^[2]

The paper's appendix gives a detailed derivation for one Maximal Cluster Graph task. The associated project page describes that example as involving 15 interdependent steps.^[4] This does not establish that every problem has exactly 15 steps, and the count should not be generalized to the full dataset.

The connection to the Strong Exponential Time Hypothesis (SETH) also requires care. Fine-grained lower-bound research shows that, for several bounded-treewidth problems, improving the base of the running-time dependence would contradict SETH.^[11] Merely solving a FormulaOne task within its expected bound does not challenge SETH. A contradiction would require a rigorously proved algorithm that crosses the relevant conditional lower bound for a problem to which that lower bound applies.

Finally, the benchmark paper was still arXiv version 1 at the July 28, 2026 research cutoff.^[1] The original scores are author-reported, and the current repository retains hidden core tests. These facts do not invalidate the benchmark, but they make independent replication, transparent attempt accounting, and dated model identifiers important when interpreting later claims.

The authors propose the task generator as a possible source of training problems for reinforcement learning with verifiable rewards, or RLVR.^[1] The released benchmark demonstrates automatic checking and controlled task structure; it does not by itself demonstrate that training on generated FormulaOne tasks improves reasoning on other domains.

References

1. ^Beniamini, G., et al. "FormulaOne: Measuring the Depth of Algorithmic Reasoning Beyond Competitive Programming." arXiv:2507.13337, submitted July 17, 2025. arxiv.org/...2507.13337
2. ^doubleAI. "FormulaOne dataset release," README at commit `151a9346bcb984b55d115271ca19f46ac74636fe`. GitHub, August 14, 2025. github.com/...README.md
3. ^doubleAI. "Release of the FormulaOne dataset." GitHub commit, August 14, 2025. github.com/...9346bcb984b55d115271ca19f46ac74636fe
4. ^doubleAI. "FormulaOne: A Benchmark for Deep Algorithmic Reasoning." Published July 17, 2025. doubleai.com/...ark-for-deep-algorithmic-reasoning
5. ^Courcelle, B. "The monadic second-order logic of graphs. I. Recognizable sets of finite graphs." Information and Computation 85, no. 1 (1990): 12-75. doi.org/...0890-5401(90)90043-H
6. ^doubleAI. "FormulaOne evaluation harness." GitHub source at commit `151a9346bcb984b55d115271ca19f46ac74636fe`. github.com/...harness.py
7. ^doubleAI. "FormulaOne few-shot prompt template." GitHub source at commit `151a9346bcb984b55d115271ca19f46ac74636fe`. github.com/...fewshot_prompt_template.jinja
8. ^doubleAI. "FormulaOne Leaderboard application source." Hugging Face Spaces. huggingface.co/...app.py
9. ^Jain, N., et al. "LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code." arXiv:2403.07974. arxiv.org/...2403.07974
10. ^El-Kishky, A., et al. "Competitive Programming with Large Reasoning Models." arXiv:2502.06807. arxiv.org/...2502.06807
11. ^Lokshtanov, D., Marx, D., and Saurabh, S. "Known Algorithms on Graphs of Bounded Treewidth are Probably Optimal." Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms (2011): 777-789. arxiv.org/...1007.5450