P0 complete · don't build it The gate was written before the work, and it passed. The recommendation is still no. This page says why.
Sell-side desks are shipping LLM-drafted analyst output, and nothing checks its numbers against the filings it cites before it goes out. A recent paper proposes the obvious control: ground every claim in filed XBRL, then have an SMT solver prove or refute the arithmetic instead of asking a second language model. I spent a week trying to falsify it against 20 real 10-Ks. Grounding held up better than expected. The proof did not — not because the solver is wrong, but because of what has to be decided before the solver is allowed to speak.
Exxon Mobil's net income attributable to shareholders was $29.8 billion in 2025.
Which filed fact is “net income attributable to shareholders”?
Both of these are tagged in the same filing, for the same period, with nothing in the data to separate them.
us-gaap:NetIncomeLoss
$28,844M
Attributable to ExxonMobil.
Z3 ⊢ 28,844 ≠ 29,800 ± 50
CONFLICT — correct. The claim is wrong.
us-gaap:ProfitLoss
$29,764M
Includes noncontrolling interests.
Z3 ⊢ 29,764 = 29,800 ± 50
VERIFIED — a false accept. The gate waves it through.
ProfitLoss is, after all, the statement's bottom line. The proof is real. It is
conditional on an accounting judgement that carries no proof, and that judgement is the
whole of what a compliance buyer would be paying for.
Not whether the paper is good — it is, and it ships working code. The question was whether the capability it demonstrates is a business: a pre-publication gate that a compliance function would buy, install, and be unable to remove.
Tying out is the practitioner's term for reconciling a figure back to its filed
source. It is the whole job here. A claim goes in, a filing goes in, and out comes
VERIFIED, CONFLICT or UNGROUNDABLE — three outcomes,
never two, because a checker that must answer yes or no on a figure it cannot locate is
guessing.
20 10-Ks from SEC EDGAR with provenance and SHA-256, spanning technology, energy, retail, healthcare, industrials and three financials. The financials are in deliberately: they are where this kind of thing usually breaks.
28 metrics taken from the standard equity-research vocabulary and applied mechanically to every filing — revenue, margins, EBITDA, FCF, leverage, returns. Choosing metrics after reading the filings is how a benchmark measures its author instead of the world.
Resolve each metric to filed facts through a concept registry, reconciling values that differ only by rounding precision, and abstaining where the binding is ambiguous. Hand what survives to Z3 as an arithmetic obligation.
Twenty realistic analyst claims, six of them wrong in ways that actually occur: wrong period, wrong concept, scale error, a segment figure passed off as consolidated. Then perturb the registry and see what the result was resting on.
This is the number that decides how big the product could be, and it is the one figure here worth trusting without qualification. 28 metrics × 20 filings = 560 attempts, no cherry-picking available. 465 ground. 95 do not.
% of the 20 filings where the metric resolves
revenue | 100% | |
|---|---|---|
net_margin | 100% | |
effective_tax_rate | 100% | |
operating_cash_flow | 100% | |
total_assets | 100% | |
eps_diluted | 95% |
% of the 20 filings where the metric resolves
rnd_intensity | 45% | |
|---|---|---|
sgna_ratio | 50% | |
inventory_turns | 50% | |
interest_coverage | 60% | |
gross_margin | 65% | |
buybacks | 65% |
Nothing exotic is happening in the right-hand column. Amazon tags no
ResearchAndDevelopmentExpense — it reports “Technology and infrastructure”.
Alphabet splits sales & marketing from general & administrative, so there is no single
SG&A line to divide by. Banks have no gross profit, no inventory, and no current/non-current
balance-sheet split at all. These are ordinary filing choices, made by filers who are complying
correctly.
| Cut | Filings | Attempts | Grounded | Ungroundable |
|---|---|---|---|---|
| All filings | 20 | 560 | 83.0% | 17.0% |
| Non-financial issuers | 17 | 476 | 88.2% | 11.8% |
| Financials (JPM, GS, BRK-A) | 3 | 84 | 53.6% | 46.4% |
The honest product scope is narrower than “verify analyst output”. It is verify standard metrics on non-financial issuers, where roughly nine in ten figures resolve. Financial-sector coverage is close to a coin flip and should not be sold. A pitch that does not say this out loud is selling something the measurement does not support.
I wrote those 20 claims after dumping each filing's facts, so I only asked about metrics I had already seen were tagged. That 0% measures my claim selection, not the world.
It is precisely the flaw I had identified in the paper's own benchmark, reproduced by accident. The census above exists to correct it.
What fraction of sentences in a real research note is numerical and checkable at all. My claim set was 2-in-20 non-arithmetic by construction, which is a design choice, not an observation.
That sets the product's value rather than its feasibility, and it needs a corpus of published notes to answer. Not done here, and it cannot be inferred from anything that was.
Six deliberately wrong claims, six correct rejections, no false accepts. Genuinely the right result, and the reason the gate passed.
It survives exactly one perturbation of the concept registry, which is the subject of the next section and the reason this page exists.
Run · 28 metrics × 20 filings = 560 attempts · 465 grounded, 95 ungroundable, 0 ambiguous · 9 of the 28 metrics ground on every filing; the worst filing grounds 46.4% of them.
The sales claim for this product is that a proved conflict is an audit trail — that is what a compliance buyer is purchasing, and it is the thing an LLM-based checker cannot offer. So the right way to attack it is not to argue with the solver. It is to ask what the solver was handed.
I reversed three preference orderings in the concept registry, each equally defensible from the
taxonomy alone: net_income resolving to ProfitLoss before
NetIncomeLoss rather than after, and the same for revenue and cost of revenue.
Nothing else changed. One claim changed outcome, and it changed the wrong way — from a
correct rejection to a false accept, the failure mode that ends the category rather than the
product.
The paper names the mechanism honestly — structural mismatches surface as solver constraint violations rather than being filtered during grounding. But its benchmark cannot exhibit the failure, because questions there are generated backwards from a declared calculation linkbase, where concept identity is supplied by the filer rather than inferred. Groundability is guaranteed by construction, and so is the binding.
The consequence is commercial, not just scientific. A compliance buyer who understands this is buying a hand-curated concept dictionary with a solver attached. That is a reasonable product. It is a completely different pitch from a formal guarantee, and it has a completely different moat — one that a competitor with a better dictionary erases.
All measured on the same 20 filings, all of them things a naive implementation gets wrong silently rather than loudly:
RevenuesNetOfInterestExpense appears nine times in a single period.Assets at both $208,160M and $208,000M in one context, at different
decimals. They reconcile as rounding once you know to look; before the grounder
collapsed them by precision, this alone produced ten spurious ungroundables.
Two of the 20 filings (Microsoft, Berkshire) ship no separate calculation linkbase file and
declare no linkbaseRef; their calculation arcs are embedded in the extension
schema instead. The relationships exist — a pipeline that looks only at the conventional path
concludes they do not. Since the paper's grounding stage and its entire benchmark
construction depend on the calculation linkbase, that is a live plumbing trap rather than a
trivium.
17.0% ungroundable against a 40% proceed threshold. Zero false accepts on six realistic wrong claims. Zero of 13 vendors shipping it. Every pre-registered criterion is met, and the gate says proceed to P1.
I am recommending against it anyway, on two pieces of evidence the gate did not anticipate because they were not known when it was written. Keeping those separate is the point: the gate's output and my judgement are different things.
A false accept ends the category. A false reject ends the product — analysts route around a gate that cries wolf, and a control nobody runs is not a control. On the paper's own human-written benchmark, its two strongest configurations falsely reject 22–24% of correct claims.
My 0% false-reject figure is not a rebuttal. I hand-parsed every assertion and handed the grounder the correct period key — which removes exactly the front end that produces those failures. It is a best case, and it is reported here as one.
Reversing a single defensible registry preference converts a correct rejection into a false accept. Zero false accepts is a property of a curated dictionary, not of the proof. The audit trail — the actual thing being sold — inherits an unprovable judgement at its base.
A mandated pre-publication approval does exist for retail-distributed and third-party research, with a registered owner. It does not cover institutional-only research, which is the core sell-side product, and no rule anywhere requires numerical tie-out. The moat is pass-mark: an incumbent could bolt grounding-plus-solver onto an existing pipeline without changing its business.
Stated as conditions, so this can be revisited without redoing the work:
UNGROUNDABLE is a
feature: it routes human attention. “Here are the 17% of figures that need your eyes” is
triage, not verification — smaller, more honest, and not killed by the false-reject problem.Three results, none of which appear to be in the literature. First, a benchmark-construction critique with a measurement attached: questions generated backwards from declared calculation linkbases make groundability a property of the construction, and the unbiased figure for a standard analyst vocabulary is 83.0% groundable overall, 88.2% excluding financials, 53.6% for financials. Second, the general result that solver-verified grounding inherits its taxonomy registry's unprovable judgements — a statement about neurosymbolic verification over taxonomies, not a bug in one paper. Third, two concrete XBRL grounding hazards, measured.
It cost a week and it answered the question it was built to answer. That is the process working, not failing. No API was written, and none should be.
All figures measured on a run of against 20 10-K filings retrieved from SEC EDGAR with recorded accession numbers and checksums. The vendor landscape is assessed from vendor-facing material only — marketing sites, product pages and third-party comparisons — not by using the products, so an unannounced feature would not appear in it. Not investment advice, not a compliance control, and not an opinion on any filer's accounting.
Every figure on this page is generated from the run's results files rather than typed by hand, and a verifier re-derives each one before deploy and fails the build if the page and the data disagree. Bar widths are checked against the numbers printed beside them, so the chart cannot contradict its own label.
The governing rule in the project is that no figure may appear in customer-facing material unless a run produced it. Where something is inferred from documentation rather than measured — the vendor landscape, the regulatory reading — the page says so in place rather than in a footnote.
This is a research note reporting a negative result. There is no product, no waiting list and nothing to buy. The recommendation it reaches is not that the paper is weak — it is careful, honest about its own limits, and ships substantive code, which is why it was worth a week.
It is also not a claim that any figure in any filing is wrong. Where two filed concepts are both defensible readings of one English phrase, that is a property of the taxonomy and of the phrase, not an error by the filer. Every issuer named here filed correctly.