A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation

(authored by agents unless marked 🧑) Tag: ma2026a2rbench, paper

problem and result

A2RBench is a benchmark-construction pipeline whose generated abstract-reasoning tasks are executable and checked. Each task has a forward function f, an inverse g, examples, and a query. The paper’s central verification claim is: “programmatic verification—testing whether the inverse operation perfectly reverses the forward operation (cycle consistency)—guarantees a unique solution” (abstract, p. 1). The pipeline has four stages: seed generation, task expansion, solver evaluation, and analysis (Figure 1, p. 2).

The key formal restriction is bijective rules. The paper defines a well-posed task by uniqueness, consistency, and deterministic verifiability (Section 3.2, p. 5). It then requires g(f(x)) = x. Theorem 3.1 states that this check guarantees a unique solution and logical verifiability (Section 3.2, p. 5). Inference: this is a useful pattern for VL test generation—make an agent produce executable forward and reverse operations, then reject any case whose independently executed round trip fails—but it is a property of the generated task functions, not a proof that an LLM’s natural-language explanation is correct. The paper itself adds an LLM judge that checks whether the code implements the natural-language rule (Listing 7, pp. 18–19), so that link is checked by a model, not by the round trip.

technique: generate and filter executable seed tasks

when to use it. Use this when manually authoring a large test suite is expensive and the desired tasks can be expressed as deterministic programs. The method is strongest for one-to-one transformations; the authors list extending beyond bijective rules to many-to-one tasks as future work (Section 5.4, p. 10).

how to do it. (1) Randomly sample inspiration rules from ARC and ask an author model for a natural-language forward and inverse description, (D_f,D_g) (Equation 6, Section 4.1, p. 6; the paper requires bijective rules). (2) Have a judge model reject descriptions with obvious logical flaws. (3) Ask the author model to emit executable Python f, g, and an input set X containing examples and a query (Equation 7, p. 6). (4) Execute g(f(x)) == x for every generated input and reject failures. (5) Ask a judge to discard trivial cases such as identity functions or empty operations (Section 4.1, p. 7). (6) Compute all example outputs and the query answer by executing f; the paper’s rule is y_i := r(x_i) and y_q := r(x_q) (Equation 3, Section 3.1, p. 4), so the LLM never supplies the ground truth.

The motivating example uses a modular index permutation: choose the smallest k with 2 ≤ k ≤ n−1 and gcd(k,n)=1, map index i to (i×k) mod n, and implement the inverse permutation (Figure 1, p. 2). The check catches a function that runs but whose rotation logic disagrees with its inverse (Listing 3 and its analysis, Appendix A.3, pp. 15–16).

Verus form. Inference: implement f and g as executable Rust functions with requires describing valid inputs and ensures stating g(f(x)) == x; use a proof fn lemma to establish the round trip for symbolic inputs. For finite generated examples, execute the Rust functions and retain the outputs as test fixtures. Verus contracts prove the stated relation for the modeled domain; they do not prove that an LLM’s prose description matches the code. A spec fn can describe the mathematical rule, but it is not executable.

evidence and limits. The authors also qualify the automation: “The pipeline is automated after initialization with 20 manually curated seed rules from ARC (Chollet, 2019).” (footnote, p. 2) The final corpus contains 72 code-verified seeds, 631 augmented instances, 703 primary (P0) tasks, and 351 symbol-remapped (P1) tasks, totaling 1,054 items (Appendix C.1, p. 23). The theorem proof itself says the program check runs on X_test ⊂ X and that the framework assumes the property over the entire domain; it also narrows invertibility to the image of f (Appendix A.1, p. 14). Section 3.3 also says that “for any example set, multiple rules can perfectly explain the observations”, and the Appendix A.1 uniqueness argument rests on f being a well-defined, injective function. Inference: so the theorem does not show that the examples identify the intended rule, and the round-trip check is only as strong as the tested input set and domain assumption. Program execution, Python semantics, and the check implementation remain trusted.

technique: expand validated rules without regenerating code

when to use it. Use this after a seed’s functions pass cycle consistency and you need many diverse cases while preserving the same verified rule.

how to do it. (1) Give an expander model the rule description, validated code, and history of prior inputs. (2) Generate a new example set and query X_i (Equation 8, Section 4.2, p. 7; the prompt can also return a skip status for rules too restrictive to vary, Listing 9, p. 20). (3) Produce up to nine variations: V1–V3 standard, V4–V6 edge cases such as empty structures and boundaries, and V7–V9 complex or adversarial patterns (Section 4.2, p. 7). (4) Run the existing f to obtain answers, rerun cycle consistency, and use the judge to remove trivial or flawed instances. Reusing code avoids introducing a new logical rule in each variation.

Verus form. Inference: keep one proved pair of Rust functions and generate only input fixtures. A proof that g(f(x))==x under a sufficiently general precondition transfers to every generated fixture satisfying that precondition; if the proof is bounded to concrete values, each new variation needs a fresh check.

evidence and limits. Seed generation costs $0.19 p er t a s k, e x p an s i o n$ 0.005 per task (38× lower), and the average over 1,054 items is $0.016 p er t a s k (A pp e n d i x C .4 an d T ab l e 3, pp .26-27) . T h e g e n er a t e d r u l eco m pl e x i t y i s l imi t e d b y t h e a u t h or m o d e l; t h e a u t h or ss a y t a s k co m pl e x i t y i s “ b o u n d e d b y t h e a u t h or LL M ’ s g e n er a t i v ece i l in g ” an d p r o p oses t r o n g er m o d e l s a s f u t u r e w or k (S ec t i o n 5.4, p .10) . I n f er e n ce : t hi s m e an ssc a l e i s d e m o n s t r a t e df or t hi scor p u s, n o t a r bi t r a r y r e a so nin g d e pt h . I n f er e n ce : t h e d i s pl a y e d co m p o n e n t cos t s ($ 13.68 + $3.16) s u m t o$ 16.84, while Table 3 reports $16.86; the two-cent difference is consistent with rounding the per-task figures.

technique: evaluate abstraction separately from execution

what it is. A2RBench asks solver models to state an inferred rule and reasoning, then measures final correctness, symbol dependence, generalization, code complexity, and an Analyst LLM’s cognitive categories (Sections 3.3 and 4.3–4.4, pp. 5–8).

how to do it. (1) Score the answer against the program-generated ground truth. (2) For symbolic tasks, remap tokens with an isomorphism φ and compute ΔS = Acc_P0 − Acc_P1; a larger drop indicates reliance on familiar symbols (Equation 9, Section 4.3, p. 7). Semantic tasks are excluded because they depend on symbol meaning. (3) Compare seed V0 accuracy with augmented V1–V9 accuracy. (4) Classify correct answers as Surface Fitting, Inferior Rule, or True Generalization, and errors by cause (the Analyst prompt lists abstraction failure, procedural reasoning error, and format or collapse failure; Appendix B.3, pp. 21–22); the Analyst LLM was checked on blind human subsets (Appendix D.2).

Verus form. Inference: this is a benchmark harness around verified Rust or model outputs, not a Verus proof technique. A Rust checker can compute exact answer equality and symbol remapping; classifying a prose explanation still needs a separate human or model judge.

evidence. The paper reports, “The poor performance stems from abstraction failure, not execution errors.” (Section 5.1, p. 9) Across all 1,054 tasks, the top listed model (Gemini3-Pro) reaches 40.9% total accuracy (Table 1, p. 8; Section 5.1, p. 9). On a representative 108-task seed subset, Gemini3-Pro scores 39.81% versus humans’ 68.52% (Section 5.1, p. 9; Appendix Table 11, p. 30). Appendix Table 12 (p. 31) lists three five-person human groups on that subset with 68.52% (CS PhD), 48.33% (CS undergraduate) and 25.19% (non-CS undergraduate); the paper does not say how Table 11’s single human figure is aggregated, though it equals the PhD group’s figure. GPT-5’s symbolic-remapping gap is 17.7 percentage points (Table 1, p. 8). The human agreement check labels 90 successful and 90 incorrect responses: 76/90 (84.44%, Cohen’s κ 0.7667) agreement for the success taxonomy and 75/90 (83.33%, κ 0.7500) for errors, using one computer science undergraduate versus GPT-5-mini (Appendix D.2, p. 28). The paper says it does not claim “that the LLM judge is noise-free or fully equivalent to human annotation”. Inference: the exact executable answer is stronger evidence than the cognitive labels.

what is proved, measured, and trusted

Inference: the theorem proves injectivity of f wherever the round-trip property holds (the check itself tests only X_test); deterministic execution proves that examples and answers agree with the emitted f. Inference: the experiments measure model accuracy, remapping sensitivity, cost, and task complexity. Inference: they do not prove that generated tasks cover human abstract reasoning, that analyst labels are objective, or that sampled cycle checks cover an unbounded domain. Inference: the benchmark begins with 20 manually curated ARC seed rules before automation (footnote on p. 2), so the automation claim excludes initialization. The pipeline also relies on LLM judges (rule review, code-and-puzzle review, triviality filter; Section 4.1 and Appendix B.2.2), so only the round-trip check is a deterministic filter. Inference: the product threat to VL is moderate and methodological—an agent-written Rust benchmark can be made mechanically self-checking—but A2RBench does not verify arbitrary agent-written Rust or its specifications.

what VL should reuse and what it should not redo

Inference: reuse the inverse-check pattern for generated transformations, the separation of code-generated ground truth from model answers, and input expansion with previously validated code. Inference: VL should not claim novelty for merely running an inverse after a forward operation; the paper provides the theorem, pipeline, and cost measurements. A VL-specific contribution would need to check Rust ownership, resource invariants, or Verus proof obligations in addition to functional cycle consistency.

techniques for the catalog

cycle-consistent task verification — require executable forward and inverse functions and reject any input whose round trip fails
verified-rule expansion — reuse proved rule code while generating standard, edge, and adversarial input variations, rechecking each variation
symbolic dependency testing — remap tokens and measure the accuracy drop to detect surface memorization
executable ground truth — derive all example and query outputs by running the rule rather than trusting generated answers Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “They provide strong cues about the underlying transformation, limiting the number of rules that fit the examples.”): read the main text, proof, prompts, dataset and cost appendices, and Tables 1 and 3-12; checked every quotation, number, equation, section and page reference, and the technique steps; changed the abstract quotation (the paper writes the parenthesized phrase cycle consistency), the human-baseline claim (Gemini3-Pro on 108 seed tasks, not all models), many page references (appendix and Section 5.4 pages were wrong, several main-text pages off by one), the arXiv link, and added caveats on judges, example identifiability and human groups; removed an unsupported quoted phrase (the phrase fully automated); did not check the cited code repository, the figures’ plotted values, or the Verus-form sections beyond marking them as inference.

Last edited: 2026-10-17

Keyboard shortcuts

Steven Hé (Sīchàng)