{"path":"research/tools-for-checking-inferences.md","content":"# What software exists to check an inference, kind by kind\n\n*2026-10-24. His question, after a reply had said \"deterministic code can check\" the shape of every kind of\ninference when the code was a trial script: \"Do massive online research on what these tasks require,\nwhether code or AI pass/harness/prompting design to optimize for what we want. If need be we'll use model\ncalls. I was just curious whether there was something like SpacY or whatever such code libraries out there,\nmaybe something in academic papers, or on GitHub these last few years, look around for a bit.\" Three\nresearch helpers' reports, saved verbatim: `tools-for-checking-inferences/report-parsers-to-logic.md`,\n`report-engines-per-kind.md`, `report-harness-design.md`. Trials run here on the project's own cases:\n`tools-for-checking-inferences/trials.py`, output beside it. Proposals AM16 and AM17 in the ledger, open.*\n\n## 0. The answer\n\n**Nothing off the shelf checks that one sentence is a rule's condition said of a term, the way spaCy tags\nparts of speech.** What exists falls into three parts, and they fit together:\n\n1. **Engines that compute what an inference of each kind implies, once it is written in their language.**\n   These exist, are maintained and are installable in Python: clingo (rules with exceptions, and listing\n   the explanations of an observation), ProbLog (rules with a stated proportion), PyArg (the argumentation\n   framework the strength layer descends from). All three ran here on our own cases (§ 3).\n2. **Parsers that turn a sentence into a structure code can compare.** None does our check end to end; the\n   nearest are a natural-logic prover (LangPro, English only) and a parser to logical boxes (UD-Boxer, not\n   Swedish). A small matcher on spaCy that I wrote today scored the same as exact matching on nineteen cases\n   (§ 2).\n3. **Ways to make the writing model comply.** The best-supported one is a checker in code that sends the\n   model a specific error and lets it revise (§ 4).\n\n**The finding that matters most for our design is that the slots avoid the literature's main failure.**\nEvery published system that checks a model's reasoning with an engine has the model write the engine's\nlanguage, and that translation is where it fails: a verifier that has the model write first-order logic\ncould check only 15–45% of chains (VeriCoT), and a model writing ProbLog unaided produced no valid answer in\nabout three cases of four (QUITE). In our design the model never writes logic. It fills slots in its own\nwords, and plain code turns filled slots into clingo or ProbLog input. What remains is whether the slots\nare filled with true sentences, and that is argued in the graph.\n\n## 1. What the corpus already held\n\nThe corpus had read the systems that have a model translate text into logic for a solver (LINC, Logic-LM,\nSymbCoT), the Natural Program format, the step metrics ROSCOE, EntailmentBank, the NLI near-miss problem\n(HANS) and two reasoning benchmarks (FOLIO, LogicBench), most of them in `one-inference-per-link/` and\n`writing-out-the-unwritten/`. Defeasible-logic engines (SPINdle, DeLP) and Carneades were named as theory.\n**None of the engines or parsers below had been installed or run before today.**\n\n## 2. Checking the form of one rule application\n\n| What exists | What it does | Fit |\n|---|---|---|\n| LangPro | natural-logic tableau prover; does A entail B; on the SICK set precision about 97.7%, recall 58–62% (helper read the full paper; I checked the paper exists and its abstract gives precision above 94%) | English only, Prolog and a grammar parser to install; untried here |\n| UD-Boxer | rule-based parser from a dependency parse to logical boxes that mark negation and quantifiers; about 82 on English | English, German, Italian, Dutch; Swedish would need four rules written; untried |\n| Attempto Controlled English (APE, RACE) | an exact check of a universal rule applied to a case, if the sentences are written in its restricted English | forces the writer into that English; no Swedish; last release 2018 |\n| Grammatical Framework | the one toolkit with English and Swedish grammars sharing one abstract form | a grammar to write; nothing recent |\n| spaCy or Stanza dependency parses, WordNet | the parts for a matcher of one's own | the only route that covers Swedish |\n\n**Trial (§ 4 of `trials.py`).** A matcher on spaCy compares each word's lemma, role and head, keeps\nnegations and quantifier words, refuses a change of tense, and treats WordNet synonyms as the same word. On\nnineteen cases I wrote and labelled, it scored 15 right, and exact matching also scored 15. It gained\n*decay* for *decomposition*, and lost a Swedish sentence that differed only by a capital letter and a full\nstop. Both refused every near-miss in the set (another subject, a negation, a tense, a leap in the\nconclusion, the wrong reference class), and both refused a correct reordering (*decomposition is what the\nsquirrel smells of*) and a correct synonym WordNet lacks (*deceased*). **So on this evidence a parser buys\nparaphrase tolerance and costs new errors; it does not yet beat exact matching.** The set is mine and tiny,\nso this is a first look, not a measurement.\n\n**What follows for the design.** Exact matching refuses a paraphrase loudly, and the refusal goes back to the\nwriter, who can repeat the rule's own words. That is cheaper than a parser and fails in the safe direction.\nThe parser earns its place only if real writers keep failing on paraphrase, which is measurable once a\nwriter runs.\n\n## 3. Checking what each kind implies\n\n| Kind | Engine | What the trial showed |\n|---|---|---|\n| Normic | clingo, PyArg (ASPIC+) | With the Griess rule and its exception written as a claim, both conclude Hill handled nitroglycerine when no exception is stated, and withdraw it when the swab touched nitrocellulose. In PyArg the exception is an undercutter of the rule, which is how the graph already treats an attack on a link. |\n| Abduction | clingo | Given Farr's two rival explanations and what each would explain, clingo lists every combination that explains the observations. With only the elevation pattern, air and water both explain it; adding the deaths around one pump leaves only explanations that include water. Two limits: it listed *both together* as an explanation too, so minimality must be asked for, and it can only choose among rivals someone wrote. |\n| Statistical | ProbLog | One rule with its proportion gives that proportion (0.33). **Two rules from two reference classes for one case gave 0.732**, ProbLog's noisy-or, which assumes the two are independent. The engine answers the reference-class question by assumption and says nothing. So the reference class must be a claim, and combining two must be a decision the graph records (the independence reading, ledger Q40), never the engine's default. |\n| Induction | FOLD-R++ / FOLD-RM (learn default rules with exceptions from tables), Popper | Untried. Our own case arithmetic (`what-a-case-counts-for/cases.py`) already does the band; these would find exceptions among filed cases. |\n| Analogy | none needed | Written as our kind requires (the respect as a rule, the target stated to have it), an analogy is a rule application, which clingo or the form check handles. The structure-mapping engine (SME) exists only in Lisp and Clojure. |\n\n**What no engine checks**: whether the rule is true, whether the exception is true of the case, whether the\nrivals written are the right ones, whether the case belongs to the reference class. Those are claims, argued\nin the graph. The engines check that the kind's logic is applied right to what was written.\n\n## 4. Making the writer comply\n\nThe harness report's five moves, ranked by evidence (sources and read tags in the report):\n\n1. **A checker in code sends the writer a specific error and lets it revise a few times.** Measured: a model\n   writing for clingo averaged 54.6% without revision and 78.0% with the solver's feedback, at about two\n   revisions (Ishay and Lee, ACL Findings 2026, Table 3, which I read in the paper myself). A model checking\n   itself does not help; the signal has to come from outside (Huang et al. 2024).\n2. **The writer reasons in prose first and fills the slots after, reasoning fields before the verdict.**\n   Already a gotcha here (*reasoning goes before the verdict*); the effect of strict formats is contested,\n   so it is tested on our own passes with the same task text in both arms.\n3. **Each inference declares the claims it starts from, and is checked against only those.** Our form check\n   already requires the case to be the first claim, an earlier conclusion or a declared premise.\n4. **No model as the gate.** Sampled candidates are filtered by code; model judges called 75–85% of\n   questions useful when 44% were (the 2025 shared task on generating critical questions).\n5. **Short per-kind instructions with one or two worked examples each, and for a normic generalization an exceptions\n   field and a separate application to the case.** A 2,600-token reference beat a 22,000-token manual;\n   most models read *usually* as *always* (Kirkpatrick and Sterken 2025, abstract checked).\n\n**What nobody has measured**: how often a model writes one inference per link against a checked form. Our own\nfigure, from published prompting, is a few in a hundred for fully atomic chains without feedback.\n\n## 5. The design this points to, and its proposals\n\n- **The writer never writes logic** (proposed as ledger AM16, *slots compile to the engines*). It reasons,\n  then fills per-kind slots in its own words; code compiles the filled slots into clingo for normic generalizations\n  and abduction, into ProbLog for a statistical generalization, and runs the form check on every rule application. A\n  combination the engine would make by default (noisy-or) is never used; combining reasons follows the\n  graph's own rulings.\n- **Every refusal goes back to the writer in words, at most three times, then the link is stored refused**\n  (proposed as ledger AM17, *the checker talks back*). AM14 already sends a refused link back once; the\n  evidence is for a few rounds with errors that name the failing slot.\n- **Exact matching stays the form check for now**; a parser is added only when real writers fail on\n  paraphrase often enough to pay for one, measured on their output.\n\nUnbuilt, all of it, except the guard for several rules on one case (§ 7). The first measurement, when his hold on keeper runs lifts, is how often the writer fills\nthe slots so they pass, before and after the checker talks back.\n\n## 7. Several rules for one case: built, ruled 2026-10-24\n\nThe red-sky trial of § 3 showed the trap: two statistical generalizations with one conclusion make ProbLog combine\nthem by noisy-or (0.732, above both rules), an independence it never states. Both signs can come from one\npassing front, and then the front counts twice. Four proposals followed, and he ruled them the same night\n(*\"Ruled. Build it please. Add it to the note also.\"*; ledger AM18, no engine combines two rules for one case):\n\n1. **The narrowest counted reference class answers alone** (Reichenbach): a counted rate for *red-sky\n   mornings with falling pressure* replaces both broader rates, and nothing is combined.\n2. **Two rules for one case never reach an engine together.** `problog_program` refuses them; the\n   combining is `accrual.combine`, adding in log-odds from the base rate only where the pair was read\n   independent (Q40, Q46), else counting as the better rule.\n3. **A pair read as one story owes a claim between** (Q42): the two support one middle claim, which supports\n   the conclusion once. Here the middle is the cause both signs point to, *a weather front is approaching*, with\n   the signs under it and *it rains today* above it; Q42 as ruled names a shared observation or a generalization,\n   so a cause as the middle was proposed as AM19 (ruled 2026-10-25). The module returns the pair and writes nothing to the graph.\n4. **A test proves the guard fires**: the red-sky pair with a shared front never comes out above the\n   stronger rule's 0.6.\n\nBuilt in `deliberus/rules_for_one_case.py` with nine tests (`tests/test_rules_for_one_case.py`); a rate\nnobody counted is set aside, per BC1. What it does not do yet: nothing calls it, since no pass writes\nstatistical generalizations in slots (AM16, open), and clingo's side, two normic generalizations for one case, has no guard yet.\nNeither engine is a project dependency; the module emits ProbLog text and computes no engine itself.\n\n## 6. How far to trust this\n\nThe engines' behaviour in § 3 was run here. The parser and harness numbers are the helpers', read from the\npapers as tagged in their reports; I opened the sources for the four that carry the argument (the clingo\nself-correction paper's Table 3, VeriCoT, LangPro, Kirkpatrick and Sterken) and each exists and says what\nwas claimed where its abstract can show it. The matcher's cases are mine.\n"}