How we measured decision model accuracy on ProofWriter

The dataset: ProofWriter

ProofWriter (Tafjord, Dalvi and Clark, 2021) is a multi-hop deductive reasoning dataset from AI2, published under CC BY 4.0. Each problem is a short theory of facts and rules in English and a statement to judge against it.

Version

V2020.12.3, official test splits: depth-0, depth-1, depth-2, depth-3, depth-5, NatLang

Gold answers

every selected label recomputed by hard_decisions.solver; zero disagreements. Our solver reproduces every published test label, on both tasks, with zero disagreements.

Pool

108,440 open-world test questions, from which the open-world sample is drawn

Synthetic

The theories are generated from templates, some reworded by people (the NatLang set). Models may have seen the dataset in training.

The sample: 1,800 problems per task, 3,600 in all

Running every model on the full test set is not practical, so the harness draws a sample with a fixed seed (0). Items are spread evenly over proof depth and the correct answer first, so deep proofs and the unknown answer are never starved the way a uniform draw would starve them; inside each cell, items are chosen to cover the other properties and spread across theories. A bigger sample with the same seed only adds items, so answers already collected stay valid.

Open world: true, false or unknown: items per depth and answer

Closed world: true or false: items per depth and answer

ProofWriter publishes no separate depth-4 split; depth-4 items come from the splits built for deeper theories.

The two tasks

The same kinds of theory under two rules for what cannot be proved. Every model got exactly this question and these options, in this order.

One request per problem, the same for every model

Each model answered each problem once, with the problem's text, the task's question and its options. Nothing was retried into a valid answer.

• Jev. Jev is a hosted decision model made by TypeSafe. We call it through its maker's software kit, typesafe-sdk, on paid API access; the version is recorded on every answer (jev-1.13.0). Its size and architecture are not published.
• GPT-6 Luna. GPT-6 Luna is a hosted large language model made by OpenAI. We used it as a classifier: one request per item through the Chat Completions API, with reasoning effort set to none (its lowest setting) and a strict JSON schema that allows only the task's options. Its size and architecture are not published.
• Kev-9B. Kev-9B is an open decision model made by Jared Palmer: a pointer head and a rank-16 LoRA adapter on a frozen 9-billion-parameter Qwen3.5 base model. We ran it on our own laptop through the Kev server on MLX, in bfloat16.
• Kev-4B. Kev-4B is an open decision model made by Jared Palmer: a pointer head and a rank-16 LoRA adapter on a frozen 4-billion-parameter Qwen3.5 base model. We ran it on our own laptop through the Kev server on MLX, in bfloat16.
• Kev-0.8B. Kev-0.8B is an open decision model made by Jared Palmer: a pointer head and a rank-16 LoRA adapter on a frozen 0.8-billion-parameter Qwen3.5 base model. We ran it on our own laptop through the Kev server on MLX, in bfloat16.
• Laya. Laya is an open decision model made by Convai Innovations: a 421M-parameter ModernBERT-large encoder with decision heads. We ran it on our own laptop with the laya package, PyTorch on Apple's GPU.

An answer that is not exactly one of the options is scored as wrong and kept in the record as given. Across every scored run so far there were 0 such answers.

Scoring

Accuracy

The share of problems answered correctly, with a 95% interval: the range the score would fall in if we drew the problems again (a percentile bootstrap, 1,000 draws, seed 0).

Floors

Chance (one over the number of options) and the best constant guess: always giving the most common correct answer in that slice.

Recall and macro-F1

Recall is the share of items with a given correct answer that the model got right; macro-F1 averages the F1 of each answer, so a model cannot score well by ignoring one.

Paired differences

Two models on exactly the same items: the difference in accuracy, with its own 95% interval. Narrower than comparing two separate intervals.

Breakdowns

Accuracy by 12 properties of the problems: proof depth, gold answer, theory kind, negation in the theory, negated statement, question strategy, paraphrased rules, theory's deepest proof, theory length, number of rules, number of facts, proof size. Only depth is controlled.

Repeatability

Each model answers every item a second time; we report agreement, Gwet's AC1 and Cohen's kappa. Details.

What the numbers cannot tell you

• ProofWriter is synthetic. Its theories are generated from templates (some reworded by people), and models may have seen it in training. It measures one kind of reasoning, not decisions in your domain.
• One protocol for every model. Each model answered each item once, with the same question and the same options. GPT-6 Luna ran with reasoning off, its lowest setting, as a direct classifier; another setting would be another model.
• Latency is not like for like. Hosted models' times include the network and the vendor's servers. Open models ran on one laptop. Compare speed within a setting, not across settings.
• Only depth is controlled. The sample balances proof depth and the answer. Other breakdowns, such as negation, length or paraphrase, move with depth and with each other: they show where errors fall, not why.
• Predictions came first. We wrote down what we expected before any model answered, and report each prediction as held or failed, including the ones we got wrong.
• Every number re-runs offline. Scores are computed from the saved answers; one command rebuilds them without calling a model. Results still being scored are marked as such, never filled in.

At about 300 items per depth, a depth's accuracy is uncertain by roughly ±5 points; at about 100 items per depth and answer, roughly ±10. Only large differences are resolvable at that level.

Run records

Every run the harness has recorded with its manifest: when, how many requests at once, on what machine and how busy it was. Earlier runs predate the manifests.

Check it yourself

Every score on this site is computed from the saved answers, offline, without calling a model. The harness rebuilds them and this site from the same files:

hd verify          # recompute every ProofWriter gold label with the independent solver
hd replay          # rescore every saved answer: studies/*.jsonl
hd report          # write RESULTS.md
cd site && npm run build    # rebuild this site from studies/, engines.yaml and the run manifests

Every number is also in one data file.

Preregistered predictions: which held and which failed

Before any model answered an item, we wrote down what we expected. Each prediction is quoted word for word and checked against the scored results, by the rule stated beside it.

14 of 22predictions held so far. 1 partly held, 14 held, 4 failed, 1 mixed, 2 pending; 1 made no claim. A pending prediction waits for results that are still being run or scored; it is never guessed.

How to read a verdict

Held

The data meets the stated rule.

Failed

The data does not.

Partly held / mixed

One part or one task held and another failed.

Pending

The results it needs are not scored yet.

The preregistration states the predictions in words. Where it does not say how a word like "falls" is tested, the rule we applied is written beside the verdict, and it is the same for every model.

The frozen design

Fixed before any model answered.

• Data: ProofWriter V2020.12.3, official test splits (depth-0,1,2,3,5 and NatLang), archive sha256
• Sample: hd build --n 1800 --seed 0 (1,800 items per semantics, difficulty-diverse, nested by seed).
• Tasks: proofwriter-owa (true / false / unknown) and proofwriter-cwa (true / false). One request per
• Engine: Jev (typesafe-sdk), model version recorded per row. A version change is a new engine.
• Primary metric: accuracy by proof depth (0 to 5) with a 95% percentile bootstrap interval (seed 0, 1,000
• Floors: chance (1 / number of options) and the best constant guesser on the same items.

What would count against us

Accuracy flat across depth (prediction 1 false), or unknown recall not the lowest (prediction 2 false), is reported as such.

Caveats stated in advance

ProofWriter is synthetic and templated, and models may have seen it in training. Interval widths at 100 to 150 items per depth are about plus or minus 8 to 10 points per class-balanced stratum, so only large differences are resolvable at the depth-by-label level. Breakdowns are descriptive, not causal.