Turning rulebooks into verified tools

We had AI agents read three real rulebooks, the NBA Collective Bargaining Agreement, the IRS Form 1040 instructions, and an airline baggage policy, and turn each into an executable Lean function with machine-checked properties. At run time an LLM only extracts the facts of a case, and the verified function applies the rules. On RuleArena, the benchmark built from these rulebooks, the tools score 90.7–100%, and every verdict traces to the rules that produced it. Along the way, the tools ended up auditing the benchmark itself.

The problem: LLMs struggle with long rule chains

RuleArena (Zhou et al., ACL 2025) tests whether a model can read a rulebook and apply it to a case. The benchmark pairs three real-world rulebooks with 816 problems, each a scenario with a ground-truth answer scored by exact match. The rules are transcribed verbatim from the primary sources: the 2023 NBA Collective Bargaining Agreement, the IRS Form 1040 instructions, and the American Airlines checked-baggage policy.

A single case from each domain shows what the task looks like in practice:

None of these is conceptually deep, but each demands that the right rules be found among many and then applied without an arithmetic slip across a long chain.

The Logos approach: spec-writer, then prover

We treat a rulebook as a specification to be formalised and proved. Two AI agents build the tool once. A spec-writer reads the source text and writes each rule as a precise, typed Lean object. A prover then fills in the decision procedure, the Lean function that decides cases, and proves the stated theorems about it. The function is then packed into a Lean executable that can be called by an LLM.

At inference time the division of labour is strict. The model reads the natural-language case and extracts the inputs. The verified tool applies the rules. Nothing about the answer depends on the model getting a long, multi-step calculation right.

Results

Exact-match accuracy by model, without and with the Logos tool, 0-shot. NBA scores the official verdict triple: legality, offending operation, offending team. Tax scores the amount owed or refunded. Airline scores the exact trip cost.

* NBA: the remaining 4.2% traces to nine disputed answer-key cases, analysed with examples below.
† Tax: the 85–91% ceiling is set by errors in the benchmark's own answer key (corrected for them: 99.7–100%), audited with examples below.
‡ Best published: Claude 3.5 Sonnet, one-shot, tier-weighted from the paper's per-level results (Zhou et al.).

Why are the numbers not 100%? Two reasons. The benchmark's own answer key is wrong or disputed in places (28 tax cases, nine NBA verdicts), which caps even the deterministic tool. The other reason is extraction. The model preparing the inputs can misread a case. In one airline run Haiku classed Vancouver as a US city, so the tool priced the wrong route and the answer came out $5 low. Wrong input, wrong output. The rules were applied correctly to wrong facts.

Why the tool has to be verified

A natural question to ask is whether LLMs can deal with the task with any tools. RuleArena tested that directly. It let the models write their own Python and execute it, turning the interpreter into an oracle calculator for the arithmetic.

Exact-match accuracy on airline tasks at difficulty level 1 / level 2, where the model writes and runs its own Python as an oracle calculator. Source: RuleArena, Table 10. These are the paper's own models, distinct from the results table above.

The paper reached the same diagnosis. The models “still make mistakes in generated codes”. A calculator removes the arithmetic slips but not the logic errors, because the tool is improvised by the model on each query and never checked. Which fee applies, which cap exception is available, which threshold is crossed: that rule logic is still guessed.

What the proofs guarantee

“Proved in Lean” can mean several kinds of guarantee. We share three out of thirteen theorems to exemplify different aspects of proof that can ensure robustness to future edits or cases not covered by unit tests.

Computational equivalence. The tax schedule is stated twice: printed “rate × income − subtraction” rows, and the progressive accumulation they summarise. bracket proves the two agree for every filing status and every nonnegative income, so a constant inconsistent with the progressive schedule fails the proof. It failed for Head of Household filing. The mismatch traced to a threshold in the benchmark’s rule text inconsistent with both the schedule and the IRS source (see the audit section later). None of the cases in the benchmark covered this error.

theorem bracket (s : FilingStatus) (x : ℚ) (hx : 0 ≤ x) :
    bracketTax s x = progressiveTax s x

A universal numerical property. monotone proves more taxable income never means less tax, for both computations Form 1040 uses: the bracket formula, and the Line 16 procedure that reads the tax table below $100,000 and the formula above it. The proof covers every table band and the switch between the two. The table prices each $50 band at its midpoint, so the property is nondecreasing rather than strictly increasing. A constant that violates it fails the build, on every future edit.

theorem monotone (s : FilingStatus) (x y : ℚ) (hx : 0 ≤ x) (hxy : x ≤ y) :
    bracketTax s x ≤ bracketTax s y ∧ ordtax s x ≤ ordtax s y

A state invariant. NBA rules are stateful. Certain signings hard-cap a team for the rest of the season, and the engine records this as a latch on the team’s state. hardcap proves that no committed run can escape it. Starting from any state satisfying the invariant, every sequence the engine commits, of any length, still satisfies it. The proof is by induction over the run. Benchmark scenarios are about three operations long. The theorem also governs step forty, where a run that would break its latch cannot commit a final state.

theorem hardcap (cc : capconstants) (s : scenario)
    (legalStep : …) (commit : …)              -- any driver instantiation
    (init : List entry) (hInit : LatchInvariant cc init) :
    ∀ (steps : List (operation × List Nat)) (final : List entry),
      -- fold over the run: apply each step, abort on any violation
      steps.foldl applyStep (some init) = some final →
      LatchInvariant cc final

Where implementation without proof can go wrong

Sometimes it would. But the RuleArena corpus shows what happens to rule implementations that nobody proves. Each of the four unproved artefacts in this story carried errors: the benchmark's reference implementation (tax), its transcribed rule text (tax), its hand-written answer key (NBA), and a small piece of unproved glue in our own stack. The proof assistant caught all four.

The tool audits the benchmark: three errors in the tax task

Run the verified calculator on all 300 structured inputs, no model in the loop, and it agrees with RuleArena's reference on 272 of 300 (90.7%). We audited all 28 disagreements by hand and attribute every one to a defect or omission in the benchmark's rule text, reference implementation, or answer key. The benchmark's code and data are public, so the audit is reproducible.

1. The answer key breaks the benchmark's own printed rule (27 of 300 cases). Form 1040 Line 22 reads "Subtract line 21 from line 18. If zero or less, enter -0-", and Line 24 adds the other taxes to it, so total tax cannot be negative. The reference implementation drops that floor. The defect is one line of micro_evaluation.py, in the function that computes the official answers:

# compute_answer(), the official-answer path — no floor:
tax_payer.computed_taxes_after_credits = (
    tax_payer.f1040_line_18 - tax_payer.computed_accumulated_credits)

So whenever a taxpayer's nonrefundable credits exceed the tax they offset, the difference is paid out as a refund. The same file applies the printed floor when grading the model's intermediate steps, contradicting its own answers. Our Lean specification captures the floor where the form states it:

-- def assembly (Form 1040 lines 22–24), verified spec:
let line22 := clip (line18Form1040 - line21)  -- "if zero or less, enter -0-"

2. The answer key applies a rule the model was never shown: the self-employment threshold (1 of 300 cases). On the real IRS Schedule SE, Line 4c ends with a waiver: “If less than $400, stop; you don’t owe self-employment tax.” RuleArena's transcription keeps the line's arithmetic and drops the waiver. The reference enforces the waiver anyway:

# compute_answer() — a rule the prompt never states:
if tax_payer.sche_se_line_4c < 400:
    tax_payer.self_employment_tax = tax_payer.self_employment_deductible = 0

This is the one case our specification misses, and it misses it deliberately. The spec is written from the prompt's rule text, and the prompt withholds the rule. Our Lean calculator therefore computes self-employment tax on any positive net earnings, exactly as the rules given to the model prescribe.

3. The proof exposed an inconsistency in the transcribed rulebook, confirmed against the IRS source as a transcription error (0 cases affected). Part of verifying the calculator is the bracket-identity theorem, which asserts that the published "rate × income − subtraction" bracket table computes the same function as the genuine progressive schedule. For Head of Household above $578,125 the proof failed, and the failure produced a counterexample: a 50-cent jump in computed tax at the printed threshold, which a progressive schedule cannot have. Checking the IRS source confirms the error is in the benchmark's prompt. This is the incorrect worksheet row the model is shown, in prompt.py, line 197:

| Over $578,125 | $TBD | × 37% (0.37) | $ 41,273.50 | $TBD | $TBD |

$578,125 is the Single filer's threshold. The subtraction $41,273.50 belongs to the genuine Head-of-Household threshold of $578,100. And the reference implementation quietly agrees with us, not with its own prompt: its bracket table uses the correct value,

if filing_status == "head of household":
    cuts = [0, 15700, 59850, 95350, 182100, 231250, 578100, 1e20]

so the text shown to the model and the oracle that grades it disagree with each other, and the failed proof is what caught it.

After confirming the discrepancy against the IRS source (Rev. Proc. 2022-38), we corrected the threshold in the specification.

There are two ways to keep score. Under our audited reading of the rules supplied to the model, the tool is right on all 300 instances and the answer key is wrong on 28 (9.3%). Judged against actual IRS law, it is correct on 299 of 300, inheriting the prompt's omission of the $400 threshold. There the key is wrong on the other 27. That is where the 99.7–100% corrected figure under the results table comes from.

The tool audits the benchmark again: nine disputed NBA verdicts

The NBA answer key is the only one produced entirely by hand. The benchmark's authors note that automated generation was infeasible for this domain. Human annotators read the CBA excerpts, wrote each scenario, decided the verdict, and listed the relevant rules, with no executable ground truth to check against.

Run the verified engine deterministically over all 216 scenarios and it reproduces 207 of the human verdicts (95.8%). We audited each of the nine disagreements individually. Our analysis attributes all nine to the answer key. Unlike the tax audit, though, arithmetic does not settle every case here.

The nine fall into two classes: four annotation defects, checkable by reading the case, and five apparent inconsistencies, where paired scenarios share every represented decision-relevant feature yet received opposite rulings (one such pair cannot both be right on arithmetic alone). We present one representative of each, as it appears in the engine's case file.

The point is not that we are right. It is that our solution can be checked. All nine disagreements are laid out this way in a stand-alone case file for review by a CBA specialist. If the specialist rules against us on a case, the fix is a rule change, and we rerun all 216 scenarios before adopting it. The engine has no per-case logic. Every rule reads only the scenario's stated facts. We change a verdict only when a written provision requires it, or when a pair of cases shows that no single rule can satisfy both. Matching more of the key beyond that would mean hard-coding individual cases. On our reading, nine of the 216 verdicts (4.2%) are wrong.

Provenance: what the agents saw, and when

The audits above are only meaningful if the specifications were not derived from the artefacts they audit. The record, per domain: