Every number below is a live ProveML claim.
The paper argues that an AI's claims should carry markup a machine can check. This page holds the paper to that: its findings are written in ProveML, and at build time the verifier resolved every marked claim against the same experiment artifacts the paper's tables regenerate from. If a run were redone and a number drifted, this page would refuse to build — it cannot say something the artifacts no longer support.
- subject a record in the artifact store
- verified equals the artifact value
- a judgment whose registered rule holds
What the verifier itself catches
Before measuring any model, the paper measures the instrument. the detection study planted 20 deliberate errors in otherwise valid markup — wrong values, wrong entities, missing context, subtle canonicalization slips — and the verifier caught 20 of them: nothing slipped through. That is a conformance test, not a benchmark; exact comparison either sees a difference or there is none.
Four models, two groups
The line between the models is stability, not rate. Phi-3 Mini (3.8B) is unstable across runs: a mean first-pass verification of 38% hides three identical runs that landed at 65, 48 and 0. A mean describes neither the runs that worked nor the one that produced nothing.
The other three sit together and stay there. Qwen 2.5 3B reaches 89% and is stable across runs; Claude Haiku 88%, stable across runs; Qwen 2.5 7B 89%, stable across runs. At three runs each, those three are not separable — the paper refuses to rank them, and so does this page.
The shape of the request, not the size of the model
On a compact, English-language finance benchmark built from real SEC EDGAR filings, the instability disappears: Phi-3 Mini (3.8B) scores 92% with a spread of just 2.5 points. Same model, same verifier, same grammar — a different request.
Translating the education prompts to English moves Phi-3 Mini (3.8B) to 60% (a shift of 22 points), and its runs become 70, 58 and 53 — the mode in which it produces nothing is gone. And context selection is not optional: given the full dataset instead of a slice, even Qwen 2.5 7B produced no verifiable markup at all — 0 constructs across the whole benchmark, while the same responses were full of numbers in plain prose.
Verified is not the same as covered
Two models can look equally trustworthy and differ enormously in how much of what they say is checkable. Claude Haiku wraps 91.9% of its numeric tokens in markup; Qwen 2.5 7B, at the same verification rate, wraps 60.5% — nearly two fifths of its numbers are unverifiable prose. Verification rate and coverage have to be read together.
Against substitution
The closest published mechanism, SymGen, has the model emit references into the data instead of values, so a wrong number is impossible — and so is reporting one. On the education benchmark it left 306 of 1392 references unresolved (22%), rendering as undefined in 41% of responses. ProveML fails on addressability too — but a failure is a flagged claim carrying the expected value, not a hole in the sentence: it flagged 212 claims on the first pass, 40 of them wrong values, a class substitution cannot produce and equally cannot report.
view this page's raw ProveML markup
<h2>What the verifier itself catches</h2>
<p>Before measuring any model, the paper measures the instrument. @[study:detection]{the detection study} planted %[injected]{20} deliberate errors in otherwise valid markup — wrong values, wrong entities, missing context, subtle canonicalization slips — and the verifier caught %[detected]{20} of them: ?[all: DETECTED_EVERYTHING]{nothing slipped through}. That is a conformance test, not a benchmark; exact comparison either sees a difference or there is none.</p>
<h2>Four models, two groups</h2>
<p>The line between the models is stability, not rate. @[model:phi3]{Phi-3 Mini (3.8B)} is ?[u: IS_UNSTABLE]{unstable across runs}: a mean first-pass verification of %[eduFirstPass]{38}% hides three identical runs that landed at %[eduRuns]{65, 48 and 0}. A mean describes neither the runs that worked nor the one that produced nothing.</p>
<p>The other three sit together and stay there. @[model:qwen3b]{Qwen 2.5 3B} reaches %[eduFirstPass]{89}% and is ?[s3: IS_STABLE]{stable across runs}; @[model:haiku]{Claude Haiku} %[eduFirstPass]{88}%, ?[sh: IS_STABLE]{stable across runs}; @[model:qwen7b]{Qwen 2.5 7B} %[eduFirstPass]{89}%, ?[s7: IS_STABLE]{stable across runs}. At three runs each, those three are not separable — the paper refuses to rank them, and so does this page.</p>
<h2>The shape of the request, not the size of the model</h2>
<p>On a compact, English-language finance benchmark built from real SEC EDGAR filings, the instability disappears: @[model:phi3]{Phi-3 Mini (3.8B)} scores %[finFirstPass]{92}% with a spread of just %[finSd]{2.5} points. Same model, same verifier, same grammar — a different request.</p>
<p>Translating the education prompts to English moves @[model:phi3]{Phi-3 Mini (3.8B)} to %[enFirstPass]{60}% (a shift of %[enShift]{22} points), and its runs become %[enRuns]{70, 58 and 53} — the mode in which it produces nothing is gone. And context selection is not optional: given the full dataset instead of a slice, even @[model:qwen7b]{Qwen 2.5 7B} ?[z: PRODUCED_NOTHING]{produced no verifiable markup at all} — %[fullctxClaims]{0} constructs across the whole benchmark, while the same responses were full of numbers in plain prose.</p>
<h2>Verified is not the same as covered</h2>
<p>Two models can look equally trustworthy and differ enormously in how much of what they say is checkable. @[model:haiku]{Claude Haiku} wraps %[eduCoverage]{91.9}% of its numeric tokens in markup; @[model:qwen7b]{Qwen 2.5 7B}, at the same verification rate, wraps %[eduCoverage]{60.5}% — nearly two fifths of its numbers are unverifiable prose. Verification rate and coverage have to be read together.</p>
<h2>Against substitution</h2>
<p>The closest published mechanism, @[baseline:symgen]{SymGen}, has the model emit references into the data instead of values, so a wrong number is impossible — and so is reporting one. On the education benchmark it left %[eduUnresolvedRefs]{306} of %[eduRefs]{1392} references unresolved (%[eduUnresolvedPct]{22}%), rendering as <code>undefined</code> in %[eduRespWithUndefinedPct]{41}% of responses. @[system:proveml]{ProveML} fails on addressability too — but a failure is a flagged claim carrying the expected value, not a hole in the sentence: it flagged %[eduCaught]{212} claims on the first pass, %[eduWrongValues]{40} of them wrong values, a class substitution cannot produce and equally cannot report.</p>
the paper (pdf, 14 pages) → · benchmarks & run artifacts → · what ProveML is →