Blog · Aug 2026
Double Agent Brings Expert-Level AI to Hardware Design
doubleAI’s Double Agent achieves state-of-the-art performance on NVIDIA’s CVDP benchmark for hardware design and optimization.
A reasoning benchmark at the level of real world mathematically complex problems, stumping all frontier AI models.
Date
Jul 17, 2025
Type
Blog
Research area
Benchmarks
Reading time
5 min
FormulaOne is a benchmark of 220 novel dynamic programming problems over graphs, in three tiers: Shallow (100), Deeper (100) and Deepest (20). The problems are grounded in Courcelle's theorem, which covers tree-decomposable graph structures expressible in monadic second-order logic.
Solving them demands a profound understanding of the problem's underlying structure: topological and geometric insight, knowledge of extremal graph theory and logic, combinatorial considerations and precise implementation. Frontier models that score strongly on existing benchmarks drop sharply beyond the Shallow tier, and none of the evaluated models solved a single Deepest-tier problem.
The benchmark starkly illustrates the gap between high performance on existing benchmarks and the deep algorithmic reasoning required for truly complex problems. The full paper (Beniamini et al., arXiv:2507.13337) has the problem construction and the model-by-model results.
Frontier AI models have recently demonstrated strong performance on mathematical and algorithmic benchmarks, including earning gold medals in olympiads, and attaining top percentile ratings in competitive programming contests. How well do such benchmarks capture the true depth of algorithmic reasoning, as it arises in real-world research problems?
We believe that existing benchmarks fail to capture the deep reasoning skills required for complex, research-level algorithmic problems. To address this gap, we introduce FormulaOne.
FormulaOne consists of 220 novel dynamic programming problems over graphs. The problems are organised into three categories, ranging from moderate difficulty and all the way up to research-level.
The latter category is incredibly demanding, requiring resolution of many points of uncertainty, and involving an array of reasoning steps, including topological and geometric insight, knowledge of mathematical domains such as extremal graph theory and logic, combinatorial considerations, precise implementation, and more.
Despite impressive performance on existing benchmarks, presently no model solves even a single 'Deepest Tier' problem.
Examples of FormulaOne problems
Two-Sum-Variant - Given an array of integers A and a target T, find two indices i, j such that A[i] + A[j] = T. Return the pair with the smallest sum of indices.
Balanced-Brackets - Given a string S consisting of characters (, ), [, ], determine whether S is a valid balanced bracket sequence.
Matrix-Diagonal-Sum - Given an n × n matrix M of integers, compute the sum of the elements on both diagonals. If n is odd, subtract the center element once.
Weighted-Interval-Scheduling - Given n intervals, each with a start time, end time, and weight, find a subset of non-overlapping intervals that maximises the total weight.
Persistent-Segment-Tree - Implement a persistent segment tree supporting point updates and range queries across Q versions, each version derived from a previous one, in O(Q log n) time and space.
Chromatic-Polynomial - Given a graph G = (V, E) with |V| ≤ 18, compute the chromatic polynomial P(G, k) using deletion-contraction, and evaluate it at k = 4.
Maximal-Union-of-Cycles - Given a tree-like graph G = (V, E) and a weight function w : V → ℕ, compute the sum of all weights of sets S ⊆ V such that G[S] is a disjoint union of cycles and S is maximal with respect to this property.
Quantum-Walk-Mixing - Given a d-regular graph G on n vertices and a continuous-time quantum walk Hamiltonian H = γA, compute the mixing time to within ε of the uniform distribution in the total variation norm.
Sheaf-Cohomology-Rank - Given a simplicial complex K and a cellular sheaf F of vector spaces over K, compute the dimension of the first cohomology group H¹(K, F).
While the problems are often natural to state, their solutions are far from obvious. The solvability of this vast class of problems is guaranteed by an algorithmic meta-theorem due to Courcelle, which broadly states:
“For every sufficiently tree-like graph, any problem definable in an expressive formal logic - Monadic Second-Order (MSO) logic - can be solved by a dynamic programming algorithm that operates in time linear in the order of the graph.”
The key is to use a structure known as a tree decomposition, which organises the graph's vertices into a series of overlapping sets, or “bags”, that are themselves arranged in a tree.
An algorithm can then traverse this tree of bags, solving the problem piece by piece using dynamic programming. This process involves designing a “state” that summarises all necessary information about the partial solution within a bag, and then defining how this state transforms as vertices are introduced, forgotten, or bags are merged.
The deceptive simplicity of the problem statements belies the extraordinary difficulty of discovering the correct dynamic programming solution. This process is riddled with subtle combinatorial and logical pitfalls, demanding a profound understanding of the problem’s underlying structure. For a detailed walkthrough of the fifteen interdependent reasoning steps required to solve a single hard problem - Maximal-Cluster-Graph - see the appendix of our paper.
All models were evaluated using their highest available reasoning settings and with the maximum context length permitted. To give models the best possible chance of success, we provide a generous few-shot prompt that covers a broad array of the ideas and techniques involved in solving these problems.
Each submitted solution is subjected to a rigorous and automated test suite that measures three key aspects of its validity:
To support research and encourage community contributions, the FormulaOne-Shallow ("warmup") dataset is released as a public resource for training and fine-tuning models. The complete test suite for all 100 'Shallow' problems is available, alongside a standalone evaluation environment, in our GitHub repository.
To maintain the integrity of the core benchmark, only a minimal subset of tests is released for the Deeper and Deepest Tier problems. Solutions submitted for evaluation on our benchmark are evaluated against a withheld comprehensive test-suite.
On the FormulaOne-Shallow problems, frontier models perform reasonably well. This confirms they have a foundational capability for these types of algorithmic tasks, in other words, the tasks are squarely in-distribution.
However, as the reasoning depth increases in the Deeper tier, and solutions require the discovery and integration of novel and more complex state representations, model performance drops off sharply.
This trend culminates in Deepest Tier, where the difficulty is characteristic of exploratory research problems. On this set of 20 problems, no current frontier model solves even a single one. This result starkly illustrates the gap that remains between high performance on existing benchmarks and the deep algorithmic reasoning required for truly complex problems.
View more at FormulaOne-Leaderboard
BibTeX
@misc{beniamini2025formulaonemeasuringdepthalgorithmic,
title = {FormulaOne: Measuring the Depth of Algorithmic
Reasoning Beyond Competitive Programming},
author = {Gal Beniamini and Yuval Dor and Alon Vinnikov
and Shir Granot Peled and Or Weinstein
and Or Sharir and Noam Wies
and Tomer Nussbaum and Nadav Schweiger
and Ido Ben Shaul and Tomer Zekharya
and Yoav Levine and Shai Shalev-Shwartz
and Amnon Shashua},
year = {2025},
eprint = {2507.13337},
archivePrefix = {arXiv},
primaryClass = {cs.AI},
url = {https://arxiv.org/abs/2507.13337}
}Keep reading
The first Code Execution Model. An agent of the machine.