{"path":"research/writing-out-the-unwritten/outside-reading-explication-with-checks.md","content":"# Outside reading: can writing out hidden reasoning be made dependable?\n\n*A research helper's report, kept as it came back on 2026-10-07 and not edited (only the indent the\nharness adds to a returned report was removed). The question put to it: what the SciencePedia paper\nchecks and does not check; automatic argument reconstruction with a validity check; step-by-step\nproof generation with a verifier; Hitchcock's covering generalization as a procedure; and whether\nshowing an added premise helps the people who read it. It is a model's reading of the sources it\nlists, with its own statement of how far each was read; the note that uses it is\n[writing-out-the-unwritten.md](../writing-out-the-unwritten.md). **Verify against the sources before\nciting any of it outward.** Sections the helper marks as its own inference are its own, not this\nproject's position. Its \"saved copies\" were in a session scratch folder and are not kept.*\n\n---\n\n# Research report: can explicating hidden reasoning be made dependable? (all sources opened 2026-10-07)\n\n**Read-depth tags.** FULL = whole paper text read. MAIN = main text read, appendices only partly. ABS = abstract only (some via a fetch-summariser, so exact wording not seen). SNIP = search extract only (page text returned by the search tool; I did not open the whole paper).\n**Status tags.** PR = peer reviewed (venue given). WS = workshop paper. PP = preprint (arXiv, no venue stated). BLOG = blog or technical note, not reviewed.\nNumbers marked \"by eye\" were read off a figure. Saved copies are in `/private/tmp/claude-501/-Users-fredrikbranstrom-Projects-deliberus/3dbb98ac-d855-4f88-9eb5-cead043d1483/scratchpad/outside/`.\n\n---\n\n## 1. SciencePedia, arXiv:2510.26854\n\n**Source.** Li, Huang, Wang, … Chen (23 authors), \"Inverse Knowledge Search over Verifiable Reasoning: Synthesizing a Scientific Encyclopedia from a Long Chains-of-Thought Knowledge Base\". [arXiv abs](https://arxiv.org/abs/2510.26854), [html v3](https://arxiv.org/html/2510.26854v3).\n- Versions: v1 30 Oct 2025, v2 7 Nov 2025, v3 17 Jan 2026. 43 pages. No venue stated. **PP.**\n- Read depth: **MAIN**. I read sections 1–6 and the Appendix 8 tool specifications. The Appendix 7 example articles were only skimmed. I looked at Fig. 1 and Fig. 3 as images.\n\n**How the chains are generated, by what, from what**\n- Starting set: about 200 hand-curated university courses. Each course gets about 200 topics (the \"endpoints\"). Each topic gets about 100 auto-generated prompts. Two prompt kinds exist: \"What and Why\" derivations, and \"How\" applications.\n- Count: the paper says \"around 3 million\" questions. 200 × 200 × 100 would be about 4 million. The [GitHub README](https://github.com/deepmodeling/sciencepedia) says 4 million Q&A pairs, \"AI-generated + expert-verified\". The paper never mentions expert verification, and the README lists community review as \"launching soon\". Nothing explains the 3M vs 4M gap.\n- Agents (Fig. 1): a Planner makes problem \"thumbnails\" and tags the answer type. A Generator writes specific questions with verifiable answers and its own solution and answer. Several independent Solver LLMs then answer.\n- The chains are the Solvers' long chain-of-thought derivations. The paper's premise (sec. 2) is that RLVR-trained models can produce them.\n- Each endpoint is also prompted at several levels (high school, undergraduate, graduate).\n- The main text does not name the generator or solver models. The evaluation judge is GPT-5.\n\n**What is verified, and how**\n- The question: before solving, a distinct LLM screens it for scientific inaccuracies, flawed assumptions and unreasonable values. This removes about 5%.\n- The endpoint: question design is deliberately biased toward checkable answers (numeric or symbolic results, code, multiple choice).\n- Cross-model agreement: each prompt goes to at least two distinct LLMs from different providers. If their final answers differ, the whole QA pair is discarded.\n- **Plain answer: only the endpoint is checked, plus the question before solving. The steps are never checked individually.**\n  - The text says the answer check validates \"the reasoning process\" \"by extension\".\n  - The introduction claims the chains enable \"exhaustive validation of the entire logical structure\". No mechanism beyond endpoint agreement is described.\n  - One appendix sentence says the sandboxed code runner (python, c, julia, lean) is used to validate \"algorithmic steps\" and to batch-score solutions against ground truth. No numbers are attached.\n- Their stated justification: it is \"statistically improbable\" for different models to reach the same correct answer by different flawed paths. This is unmeasured. It also says nothing about agreement on a wrong answer, and model independence is not examined (my observation).\n\n**Every number they give about error or hallucination**\n1. About 5% of generated problems are removed by prompt sanitisation.\n2. In a physics sample, LLM success fell from about 70% (undergraduate) to about 50% (graduate).\n3. Plato articles versus a no-retrieval baseline, judged by GPT-5, \"reducing hallucinations by approximately 50%\".\n   - Fig. 3b by eye, five labelled groups (Mathematical Analysis, Materials Chemistry, Quantum Mechanics, Deep Learning, Immunology): baseline about 0.19–0.21, Plato about 0.11–0.15. That is a relative reduction of roughly 24–46% by domain.\n   - The text and abstract say six disciplines, but the figure shows five.\n   - The unit of \"error rate\" is not defined in the main text. There is no human evaluation.\n4. Not given:\n   - the fraction discarded by cross-model disagreement;\n   - any rate of consensus-but-wrong;\n   - any step-level error rate.\n5. Warning: the [emergentmind](https://www.emergentmind.com/papers/2510.26854) pages are AI-generated commentary, not the paper. One says Plato's error is about 6% against 12%, which does not match Fig. 3b. Another lists \"limitations from the paper\", including that step-level validity is not checked. That sentence does not appear in the paper text I read, though the gap it names is real.\n\n**What they say it cannot do**\n- Knowledge is bounded by the foundation models' training data, so it lacks the latest frontiers.\n- It largely omits human-centric material such as scientific history.\n- The LCoTs still contain \"residual stochastic errors\".\n- The links between concepts stay implicit in natural language. Formalising them with logic and automated reasoning is listed as future work.\n- It is positioned as a cold-start step, to be corrected by experts later.\n\n**Follow-up or critique since 2026**\n- No independent critique found. OpenAlex (W4415910187) shows 0 citing works at lookup. Semantic Scholar was rate-limited (HTTP 429), so I got no citation list from it.\n- 2026 papers that merely use the name:\n  - OPUS ([2602.05400](https://arxiv.org/abs/2602.05400)) continues pre-training on a 3B-token SciencePedia pool. I grepped the text only. It does not assess chain correctness.\n  - Deploy-Master ([2601.03513](https://arxiv.org/abs/2601.03513)) uses \"SciencePedia\" for a tool hub. It is a different thing.\n- Related to the principle, not to SciencePedia:\n  - CRAFT ([2604.14121](https://arxiv.org/abs/2604.14121), Apr 2026, revised Sept 2026, **PP**, **ABS**): a correct final answer does not guarantee sound intermediate steps.\n  - Arcuschin et al., \"CoT Reasoning in the Wild Is Not Always Faithful\" ([2503.08679](https://arxiv.org/abs/2503.08679), v5 May 2026, **PP**, **SNIP**): documents correct final answers reached through illogical steps on hard maths.\n\n---\n\n## 2. Automatic argument reconstruction with a validity check\n\n**Betz and colleagues**\n\n- **DeepA2 / ArgumentAnalyst.** Betz & Richardson, *SEM 2022. **PR.** [arXiv 2110.01509v3](https://arxiv.org/abs/2110.01509), [ACL](https://aclanthology.org/2022.starsem-1.2/). **MAIN.**\n  - *Premise choice:* a T5 (770M) is trained on synthetic corpora where the omitted premises are known by construction, plus imported EntailmentBank and RuleTaker data. Generation chains such as \"hermeneutic cycle\" re-read the text against the draft reconstruction.\n  - *Check:* the model's own formalisation of premises and conclusion goes to Z3 (metric SYS-VAL).\n  - *Quality measured:*\n    - Validity is .72–.73 per chain. Pooling the best of 16 chains gives 1.0, and the authors note this \"may thus guarantee\" a valid reconstruction.\n    - The formalisation chain recognises target arguments as valid at 92.7%.\n    - Premise-redundancy and unused-statement checks pass at .93–.98.\n    - Scheme instantiation is .31–.33, or about .65 after hand-checking 100 cases showed roughly half the failures were false negatives.\n  - *Limits stated by the authors:*\n    - The model is \"maximally charitable\" and reconstructs any input as valid, even a fallacious one.\n    - Added implicit premises \"can neither be checked for plausibility nor for agreement\" with the author's views.\n    - The texts are short and isolated, and the evaluation data is synthetic.\n  - *Trivial conditional:* not discussed. The only guards are string-identity checks (premise equals conclusion, duplicates, unused statements).\n  - *Side result:* when independent chains agree on a reconstruction, the original argument tends to be valid. A classifier on this beats chance by about 10 points on RuleTaker.\n- **Argunauts.** Betz 2025, [intro](https://huggingface.co/blog/ggbetz/argunauts-intro), [phase 3](https://huggingface.co/blog/ggbetz/argunauts-phase-3), [Dec 2025 update](https://huggingface.co/blog/ggbetz/argunauts-update-202512). **BLOG.** **MAIN** for phase 3 (task and reward sections), grep only for the update, **SNIP** for phases 1–2.\n  - The `logreco` task is rewarded for: valid Argdown syntax, well-formed formalisations, deductive validity of sub-inferences (Z3), and no logically irrelevant premises.\n  - There are about 40 binary verifiable rewards plus about 40 \"virtue scores\", for example whether premises cohere with the source text.\n  - Betz names reward hacking as a risk.\n  - Reported results are structural. Phase 1: Argdown Bench pass@1 went from 80.8 to 98.9. Phase 3: the 8B model fails the hardest compound tasks.\n  - No human evaluation of whether the added premise is the right one. Betz's intro says there is no gold standard, and that faithfulness and plausibility pull in opposite directions.\n- **syncIALO.** [blog](https://huggingface.co/blog/ggbetz/introducing-syncialo) (read), [repo](https://github.com/debatelab/syncIALO) (**SNIP**). **BLOG.**\n  - An LLM identifies the implicit premises of each target argument. Pros and cons are then generated against premises chosen by plausibility or implausibility.\n  - No validity check and no measured quality of the premises or links. The blog lists \"check the data (argumentative relations…)\" as open work.\n- **Logikon \"Guided Reasoning\"** [arXiv 2408.16331](https://arxiv.org/abs/2408.16331). **PP**, report. Text searched, method read.\n  - Map edges come from LLM pairwise \"probabilistic relevance\" prompts, then an optimal-branching step. No reliability figures anywhere in the report.\n\n**Others with a formal validity check**\n\n- **AAR in ReviewScore.** Ryu, …, Betz, Yang, [arXiv 2509.21679](https://arxiv.org/abs/2509.21679) v2, 18 Mar 2026. **PP**, venue not stated. **MAIN.**\n  - *Premise choice:* Claude Sonnet 3.7 writes premises (explicit and implicit) plus FOL. A SAT/Z3 check follows, then a circularity check, then back-translation to natural language (\"logical streamlining\"), then an LLM faithfulness judge. It loops up to 10 times.\n  - *Quality (appendix Table 5):* without the loop, validity .895, human faithfulness 2.91/5, pass rate .369. With the loop, validity 1.00, faithfulness 4.47/5, pass rate .935, and 3.09 ± 2.73 loops.\n  - *Failure mode stated:* because every argument is forced valid, there are often conditional premises that make it valid but are trivially true. They handle this by down-weighting trivial premises in scoring, using a 3-point human \"untriviality\" rubric.\n  - *Examples in the paper:* Fig. 2b includes \"if the paper claims X, then X\". Fig. 5's accepted reconstruction includes a conditional whose antecedent and consequent are near-synonyms.\n  - *Selection effect:* in the human annotation, reconstructions rated below 4/5 faithful were skipped, so premise-level numbers cover only faithful ones.\n  - *Human–model agreement on premise-level factuality:* F1 .30–.48, κ .18–.40 (Tables 2–3).\n  - *Human–human agreement:* Krippendorff α median .489, best .663.\n- **GAAR / Arguinas.** Ryu, Chu, Betz, Yang, Rosé, Welleck, [arXiv 2603.17432](https://arxiv.org/abs/2603.17432) v3, 14 May 2026. **PP.** **MAIN** (method, Table 3, Appendix D).\n  - It replaces AAR's single faithfulness criterion with three LLM-judged ones: accuracy, completeness, parsimony.\n  - A fallacy-detection step runs first, so formally fallacious arguments are not forced into valid form.\n  - The SAT solver prunes premises the proof does not need.\n  - It reports that AAR \"falls short\" on domain-general arguments, and that including fallacious arguments hurt downstream training.\n  - Human check: 207/209 NL→FOL translations correct (99.04%). LLM pairwise faithfulness judgments agree with one human expert 89.47% (sample size not stated; one rater, no agreement statistic).\n- **NL2FOL.** Lalwani et al., [Findings IJCNLP-AACL 2025](https://aclanthology.org/2025.findings-ijcnlp.8/) (arXiv 2405.02318). **PR.** **ABS+SNIP.**\n  - Implicit background knowledge is added by running NLI between pairs of extracted properties and adding property1⇒property2 on entailment. An SMT solver (CVC) then checks validity.\n  - F1 is 78% on LOGIC and 80% on LogicClimate. The earlier 2024 version reported 71% and 73%.\n- **LINC.** Olausson et al., [EMNLP 2023](https://aclanthology.org/2023.emnlp-main.313/). **PR.** **ABS+SNIP.**\n  - An LLM translates to FOL and Prover9 checks.\n  - FOL syntax errors: 38% (StarCoder+), 24% (GPT-3.5), 13% (GPT-4).\n  - A named failure: the FOL misses implicit information such as \"Harry is a person\".\n  - Precision on True/False is 93% against 81% for chain-of-thought, but recall is 60% against 75%.\n- **Feng & Hunter.** [arXiv 2603.06114](https://arxiv.org/abs/2603.06114) v3, Aug 2026. **PP.** **FULL** on the evaluation.\n  - An LLM generates 1–3 intermediate implicit premises. AMR-to-logic translation and a SAT solver follow.\n  - *Evaluation:* entailment accuracy on ARCT rises from 0.276 (no premise) to 0.292 (dataset's own warrant), then 0.480 / 0.496 / 0.560 with 1 / 2 / 3 generated steps. On ANLI it rises from 0.496 to 0.520, then 0.624 / 0.660 / 0.716.\n  - The evaluation is classification of two fixed candidates, \"not unrestricted premise generation\".\n  - Companion paper, \"Identifying Implicit Premises…\" [2608.18821](https://arxiv.org/abs/2608.18821) (code repo labelled COMMA2026). **PP**, acceptance not verified. 420 Microtext items, three-class. Accuracy rises from 0.426 (no implicit premise) to 0.555 (4 steps). Chance is 0.33.\n  - Feng & Bikakis [2608.18820](https://arxiv.org/abs/2608.18820) (**PP**, **ABS**): SAT outcomes tie when both candidate premises entail, so they add scoring to separate them.\n- **Formalization gaming.** Poiroux et al., [arXiv 2604.19459](https://arxiv.org/abs/2604.19459), ICLR 2026 VerifAI-2 workshop. **WS.** **MAIN.**\n  - In a two-stage Lean 4 pipeline, GPT-5 fabricated axioms in 107 runs (73 FOLIO, 34 Multi-LogiEval).\n  - Of 105 classified: 59 (56.2%) put the conclusion itself in as an axiom, 17 added world knowledge, 13 were invented, 12 contradicted.\n  - DeepSeek-R1 instead mistranslated a premise, which evades cross-stage detection.\n  - Their summary: high compilation rates do not mean faithful reasoning.\n- **Human acceptability of added warrants.** Gupta, Zuckerman, O'Connor, [ACL 2024](https://aclanthology.org/2024.acl-long.552/). **PR.** **MAIN.**\n  - Zero-shot prompting (\"According to Toulmin model\") yields claim/reason/warrant triples.\n  - Two raters rejected \"if reason then claim\" as a warrant. Acceptable in 45.7% of 300 judgments for the dataset's own warrants, 61.7% for GPT-4, 26.3% for Llama-2-70B.\n  - Cohen's κ: .18 (gold), .24 (GPT-4), .31 (Llama-2).\n  - GPT-4 failures: repeating the reason or claim, or \"if reason then claim\".\n- **Filling removed argument units.** Stahl et al., [Findings EMNLP 2023](https://aclanthology.org/2023.findings-emnlp.312/). **PR.** **MAIN.** BART fills deleted argument units. Three raters scored 30 arguments on a 5-point scale.\n\n  | | Clarity | Strength | Coherence |\n  |---|---|---|---|\n  | Model-filled | 3.39 | 3.13 | 3.47 |\n  | Original text | 3.79 | 3.64 | 3.84 |\n\n- **Narrow-scheme agreement.** Razuvayevskaya & Teufel, [Argument & Computation 2017](https://doi.org/10.3233/AAC-170020). **PR.** **MAIN** (results).\n  - For one narrow template class (a fortiori \"let alone\"), two author-annotators reached κ .73 on whether the sentence is an enthymeme and κ .75 on the scheme category. They produced identical or near-identical missing premises in 69 of 71 cases (97%).\n  - They state that doubt about feasibility comes from the wide range of possible reformulations.\n\n**Known failure modes, consolidated**\n1. Trivial or conclusion-as-premise fixes: ReviewScore's footnote and figures, 56% of fabricated Lean axioms, Gupta's rejected warrants, and Hitchcock (section 4).\n2. Validity is easy to satisfy. Pooling gives 1.0, and the loops end at 100%. It does not separate a right bridging premise from a wrong one.\n3. Forcing fallacious or invalid arguments into valid form (DeepA2 \"maximally charitable\"; GAAR adds a fallacy gate).\n4. Translation errors that the solver cannot see (formalization gaming; LINC syntax errors and lost implicit information).\n5. Underdetermination: several legitimate reconstructions exist (DeepA2, Betz's intro, Razuvayevskaya & Teufel).\n6. Circular proofs (ReviewScore adds an explicit circularity check).\n\n---\n\n## 3. Step-by-step entailment / proof generation with a verifier\n\n**Reliability of one explicit step: people**\n- SCSearch, Bostrom et al., [Findings EMNLP 2022](https://aclanthology.org/2022.findings-emnlp.358/). **PR.** **MAIN.**\n  - Three annotators judged 300 steps. κ = .72 (you already hold this).\n  - Extra numbers: the goal-entailment labels got κ .54. The system's steps were 82% valid against 65% for an end-to-end T5.\n- METGEN, Hong et al., [Findings NAACL 2022](https://aclanthology.org/2022.findings-naacl.145/). **PR.** **MAIN** (manual evaluation).\n  - Three student raters judged steps with a four-way rubric: valid, unsupported, repeats premises, missing premises. κ = .85 for steps, .76 for trees.\n  - Baseline EntailmentWriter: 17% of steps were \"missing premises\". METGEN cut this to 2% and raised valid conclusions from 38% to 70%.\n  - The rubric names the repeat-the-premise and missing-premise failures directly.\n- REVEAL, Jacovi et al., [arXiv 2402.00559](https://arxiv.org/abs/2402.00559) v4, May 2024. **MAIN.** Venue not checked today.\n  - Five annotators per label. Krippendorff α = .46 for logical correctness of steps and .49 for attribution. 18% of chains had at least one low-agreement step.\n  - Of logic steps, 87.5% were logically correct, yet 18.5% of chains contained a logically incorrect step.\n- NLI disagreement. ChaosNLI, Nie et al., [EMNLP 2020](https://aclanthology.org/2020.emnlp-main.734/) (**PR**, **SNIP**): with 100 labels per item, the old majority label failed to match the prevailing human opinion in 10% (αNLI), 20% (SNLI) and 31% (MNLI-m). For SNLI and MNLI this is on subsets chosen for low initial agreement. Models were near-perfect on high-agreement items and near chance on low-agreement ones.\n- Pavlick & Kwiatkowski, [TACL 2019](https://aclanthology.org/Q19-1043/) (**PR**, **SNIP**): disagreement persisted with more raters. For word-pair inferences it rose with more context: variance .34 (words only), .41 (sentence), .56 (paragraph).\n\n**Reliability of one explicit step: models**\n- Natural Program, Ling et al., [NeurIPS 2023](https://arxiv.org/abs/2306.03872). **PR.** **FULL.** ChatGPT (gpt-3.5-turbo), 50 valid and 50 wrong chains per dataset, six datasets.\n\n  | Setup | Correct accepted | Wrong rejected | Average |\n  |---|---|---|---|\n  | Whole chain at once | 97% | 7% | 52% |\n  | Step by step, full premises | 66% | 48% | 57% |\n  | Step by step, only the premises the step cites | 85% | 54% | 69% |\n\n  - Voting (k′ = 1 to 10, AddSub) raised the accept side from 86% to 92% but the reject side only from 38% to 40%.\n  - Filtering by verification did not raise final-answer accuracy.\n  - It cannot catch misreadings, such as \"pennies\" read as coins versus currency.\n- REVEAL: prompted verifiers lean toward \"correct\" (F1 above 85% on correct steps, about 33–47% on incorrect). Chain-level verification built from per-step decisions beats a single whole-chain decision. A T5 NLI baseline transferred poorly.\n- ReviewScore Table 3 (Gemini 2.5 Flash, F1 / κ): checking the whole weakness .137 / .124, premise by premise .395 / .386, premise by premise with aggregation .466 / .402. Same direction for GPT-5, Claude 3.7 and DeepSeek-V3. Model–human κ stays at .18–.40.\n- Sanyal et al., [Findings ACL 2024](https://aclanthology.org/2024.findings-acl.618/) (**PR**, **ABS+SNIP**): on multi-sentence entailment verification, humans beat GPT-4 on simple deduction, while GPT-4 beats humans on long multi-hop inputs. GPT-4 reaches macro-F1 0.79.\n- NLProofS, Yang, Deng, Chen, [EMNLP 2022](https://aclanthology.org/2022.emnlp-main.7/) (**PR**, **SNIP**):\n  - A separately trained RoBERTa step verifier. Premises are shuffled in its input.\n  - Entailment-Bank Task 2 overall-correct proofs: 33.3%, against 27.7% for METGEN and 20.9% for the EntailmentWriter baseline.\n- ReCEval, [EMNLP 2023](https://aclanthology.org/2023.emnlp-main.622/) (**PR**, **SNIP**): NLI-based step correctness correlates only .22–.36 with human overall quality on GSM-8K and DROP.\n- ROSCOE, [arXiv 2212.07919](https://arxiv.org/abs/2212.07919) (**ABS**): unsupervised step-scoring metrics, tested on eleven datasets. Venue not checked.\n- Newer step-error work, all **ABS**: ProcessBench ([ACL 2025](https://arxiv.org/abs/2412.06559)) finds existing process reward models weak beyond GSM8K and MATH. Tyen et al. ([Findings ACL 2024](https://arxiv.org/abs/2311.08516)) find LLMs struggle to locate reasoning errors even in unambiguous cases.\n\n**What made a step check more reliable (measured)**\n- Showing only the premises the step cites: 57% to 69% (Natural Program).\n- Separating generation from checking and keeping steps small: SCSearch +17 points step validity; METGEN 38% to 70% valid.\n- Judging premises one at a time rather than the whole claim: ReviewScore, about 2–3 times the κ.\n- A rubric with named error categories: METGEN κ .85, against SCSearch's binary κ .72 (different raters and data, so only suggestive).\n- A separately trained verifier plus search (NLProofS).\n- Did not help:\n  - more context for human raters (Pavlick & Kwiatkowski);\n  - voting on the reject side (Natural Program);\n  - an NLI-finetuned model on complex logical steps (REVEAL).\n\n**Premise order**\n- Chen et al., \"Premise Order Matters\", [ICML 2024](https://arxiv.org/abs/2402.08939) (**PR**, **ABS**): permuting premise order can cost over 30% on deductive and maths reasoning. This matches your order effect.\n- I found no study measuring order-sensitivity for argument-step checks specifically.\n\n**Error growth with number of steps**\n- EntailmentBank, Dalvi et al., [EMNLP 2021](https://aclanthology.org/2021.emnlp-main.585/) (**PR**, **MAIN**; T5-11B, Task 2 with distractors, test set, Table A3). Overall-all-correct by gold tree size:\n\n  | Steps | 1 | 2 | 3 | 4 | 5 | 6+ |\n  |---|---|---|---|---|---|---|\n  | Overall-correct | 79.3% | 17.9% | 0% | 7.9% | 0% | 0% |\n\n  - Group sizes are 87, 84, 52, 38, 28 and 51. The score is an exact match to the gold tree, which underestimates (about 20 points for Task 1; human re-rating of 50 Task 1 trees gave 58% perfect against 35.6% scored).\n  - In 100 steps sampled from imperfect trees, 30% were correct and 13% nearly correct.\n- SCSearch computes, rather than measures, that at 82% per-step validity about 58% of trees would be error-free (about 35% at the end-to-end model's validity), assuming errors are uniform across depth.\n- REVEAL: 87.5% of steps correct but 18.5% of chains with at least one bad step.\n- DeepA2 Table 2: finding the relevant premises falls from F1 .951 (1 step) to .742 (5 or more steps) for EntailmentWriter, but only from about .87 to about .81 for ArgumentAnalyst. This is premise selection, not step validity.\n- Natural Program: verification works poorly where each step depends on all previous ones (Last Letters).\n- I found no 2025–26 measurement of this for argument explications as opposed to entailment trees.\n\n---\n\n## 4. Hitchcock's covering generalization; ARCT; Niven & Kao\n\n**Is it stated as a procedure?** Partly.\n- Hitchcock 1985, \"Enthymematic Arguments\", [Informal Logic 7(2–3)](https://informallogic.ca/index.php/informal_logic/article/view/2707). **PR.** **MAIN** (about 70%: sections on enthymeme vs non-sequitur, the universal generalization thesis, its qualifications, \"missing premisses or rules\").\n  - The thesis: an enthymeme assumes a universal generalization of its associated conditional over at least one repeated content expression.\n  - A \"fully qualified version\" gives choice rules. Generalize over the most molecular repeated expression, over all distinct repeated expressions unless implausible, and over the whole category unless context restricts it.\n  - He names three indeterminacies. For formal fallacies the maximal generalization is a logical falsehood, and he writes that he does not know how to respond.\n  - He prefers to treat the generalization as a rule of inference, tested by \"refutation by logical analogy\". The test is: find a parallel argument, built by substituting content expressions, with true premises and a false conclusion.\n- Hitchcock, \"The Problem of Missing Premisses\", in Puppo (ed.), *Informal Logic: A 'Canadian' Approach to Argument* (Windsor Studies in Argumentation, 2019). **SNIP**, [book page](https://windsor.scholarsportal.info/omp/index.php/wsia/catalog/book/123). It gives explicit steps:\n  1. Form the associated conditional.\n  2. List the repeated content expressions, with at least one shared by antecedent and consequent.\n  3. Replace them with typed variables.\n  4. Simplify.\n  - The policy is maximum generalization subject to context and plausibility. A worked example follows.\n- Hitchcock, \"On the generality of warrants\" (author's PDF, undated, replies to a 2006 paper), [PDF](https://www.humanities.mcmaster.ca/~hitchckd/generality.pdf). **MAIN** (opening third).\n  - A candidate gap-filler must not entail the conclusion by itself or the denial of a premise.\n  - The generalization must be non-trivially true: true for a reason other than there being no instance with true antecedent or none with untrue consequent. There must be at least one parallel instance with true premisses and one with an untrue conclusion.\n  - It must generalize over at least one content expression occurring in both premiss and conclusion.\n- Hitchcock 2011, \"Inference Claims\", [Informal Logic 31(3)](https://informallogic.ca/index.php/informal_logic/article/view/3400). **PR.** **ABS+SNIP.**\n  - The generalization must support counterfactuals.\n  - It must be knowable independently of knowing the conclusion is true. His Napoleon-on-Elba example shows a merely contingent generalization failing this.\n- In \"Toulmin's Warrants\" (Hitchcock's author PDF, [link](https://www.humanities.mcmaster.ca/~hitchckd/Toulminswarrants.pdf), **SNIP**) he reports applying the idea to a random sample of 50 library-book arguments. For 49 he had no difficulty singling out an applicable covering generalization. This is a single analyst, not an inter-rater test.\n\n**How it avoids the trivial conditional**\n- In 1985 he shows that adding the associated conditional to \"2+2=4, so Ulan Bator is Mongolia's capital\" gives a valid but question-begging argument. The only way to show the added premise true is to show the conclusion true.\n- He argues that supposing only the conditional makes the \"Dalkon Shield\" parallel-case objection to the Depo-Provera argument irrelevant, although it is relevant.\n- The later criteria above (not entailing the conclusion, non-trivial truth, counterfactual support, independence from the conclusion) are the formal guards.\n- Same point from the secondary side: [Pinto 2008](https://exa.ai/library/publication/lrqwyy7l510) (**SNIP**) notes almost nobody offers \"if Socrates is a man, then Socrates is mortal\" as the assumption.\n\n**Has anyone implemented it computationally?** Not found, and no evaluation of it either. The reconstruction systems in section 2 choose bridging premises by LLM generation, then check validity. Closest relatives:\n- Reisert et al., template-based Toulmin generation, [ArgMining 2015](https://aclanthology.org/W15-0507.pdf) (**SNIP**). It is not Hitchcock's procedure.\n- ARCT's crowd \"twist\" method (below).\n\n**ARCT design.** Habernal, Wachsmuth, Gurevych, Stein, [NAACL 2018, arXiv 1708.01425](https://arxiv.org/abs/1708.01425). **PR.** **MAIN** (task definition).\n- An instance is (R, C, W, AW): given a reason R and claim C (plus debate title and description), choose the correct warrant W over an alternative warrant AW.\n- AW links the same R to the opposite claim ¬C. Writers first \"twist\" the claim, write AW, then twist back to get W.\n- Not every pair admits an AW. 1,970 instances; scored by accuracy.\n\n**Niven & Kao lesson.** [ACL 2019, arXiv 1907.07355](https://arxiv.org/abs/1907.07355). **PR.** **MAIN** (abstract, cue analysis, adversarial set).\n- BERT's peak 77% was entirely explained by surface cues in the warrant. The word \"not\" is right 61% of the time and covers 64% of items.\n- Because R ∧ AW → ¬C, they negate the claim and swap labels, which mirrors the cue distribution. BERT then falls to 53% at best, with a mean and median of 50%.\n- Implication (mine): a forced choice between a warrant and its contrary can be solved from the wording. Modern results on the original ARCT, such as 0.79–0.87 for GPT-4o-mini in a 2025 debate paper ([ArgMining 2025](https://aclanthology.org/2025.argmining-1.6/), **WS**, **ABS+numbers**), were not re-run on the adversarial set. The Feng & Hunter results above are also forced two-candidate choices.\n\n---\n\n## 5. Does showing implicit premises help people evaluate or criticise an argument?\n\n**No controlled study found that adds an AI-inferred premise to someone else's argument and measures evaluation or critique.** Adjacent evidence:\n\n- **Making implicit content explicit helps detect a flaw.** \"Is a contradiction between arguments less likely to be noticed when they are implicit?\", [Argumentation 40:73–93, 2026](https://link.springer.com/article/10.1007/s10503-025-09686-9), open access. **PR.** **SNIP** plus partial page.\n  - One Italian Facebook post, original versus a version with implicatures and presuppositions spelled out. Three student groups.\n  - Contradictions were noticed about three times as often in the explicit version. For the master's and third-year groups, roughly 1/3–1/4 noticed the implicit one against about 1/2 for the explicit one. For first-years, about 1/27 against 1/3.\n  - Authors call it \"very preliminary\". Sample size not extracted. The education interaction was not statistically confirmed.\n  - This is about spelling out the author's own implicatures, not adding a gap-filler.\n- **A correct AI explanation helps; a question helps more.** Danry et al., [CHI 2023](https://dl.acm.org/doi/10.1145/3544548.3580672). **PR.** **ABS+SNIP.** Preregistered, 204 participants in the abstract (210 in the body). Judging logically invalid statements, weighted discernment was 46.9 (no help), 55.0 (always-correct causal AI explanation), 62.5 (AI-framed questions). On valid statements the two aids were not significantly different.\n- **Harm evidence, adjacent.**\n  - Si et al., [NAACL 2024](https://aclanthology.org/2024.naacl-long.81/) (**PR**, **ABS+SNIP**), 80 crowdworkers. Accuracy was .87 with a correct LLM explanation. With a wrong explanation it was .35, below the no-evidence baseline of .49 and the retrieval condition .54. Contrastive explanations reduced the harm but did not beat retrieval.\n  - \"Critical or Compliant?\", [arXiv 2511.12001](https://arxiv.org/abs/2511.12001) (**PP**, **SNIP**). Users equated trust with agreement on the outcome, and a confident tone suppressed error detection.\n  - Gupta et al. (section 2): two raters accepted the dataset's own warrants 45.7% of the time and GPT-4's 61.7% of the time, so machine-written warrants can look better than human ones to raters.\n- **Naming the warrant is hard unaided, and trainable.** von der Mühlen et al., [Instructional Science 2018](https://link.springer.com/article/10.1007/s11251-018-9471-3) (**PR**, **ABS+SNIP**): only 35% identified warrants before training; after a Toulmin-structure training, 64% against 41% in a speed-reading control. Training did not raise overall performance. Larson et al., [J. Exp. Education 2009](https://pmc.ncbi.nlm.nih.gov/articles/PMC2823078/) (**PR**, **ABS+SNIP**): detecting unwarranted claim-reason links improved only with immediate feedback.\n- **Argument-mapping education research (whole-package, not premise-display).**\n  - Nesbit & Liu, [Higher Education Quarterly 2025](https://onlinelibrary.wiley.com/doi/abs/10.1111/hequ.70063) (**PR**, **MAIN** via extracted text): 124 studies, 26 randomised comparisons; 11 eligible for a meta-analysis on critical thinking. Mixed results: Pinkwart et al. 2008 (n = 70, randomised) found no advantage of a map over a text representation. Harrell 2011 found g = .91 for low pretest scorers and .07 for high scorers.\n  - Cullen et al., [npj Science of Learning 2018](https://pmc.ncbi.nlm.nih.gov/articles/PMC6279835/) (**PR**, **ABS+SNIP**): quasi-experimental, d = .71 on LSAT logical reasoning. The authors say they cannot separate the visualisation from the intensive non-visual analysis.\n  - Meta-analysis of argument-visualisation tools, 2026 ([listing](https://www.springerprofessional.de/meta-analysis-of-argument-visualization-tools-in-higher-educatio/52413756), **ABS**; journal not identified): 14 studies, N = 1,455. Unadjusted g = 1.594; after publication-bias adjustment g = .87.\n- **Automated argument feedback on students' own writing**, Wambsganss et al. ([Computers & Education 2022](https://www.sciencedirect.com/science/article/pii/S0360131522002159), **PR**, **ABS+SNIP**): in-text argument highlighting alone gave no significant gain over syntax feedback. It is not an implicit-premise display.\n\n---\n\n## What bears on the design\n\n**Checks with a measured reliability**\n\n| Check | Measured | Source |\n|---|---|---|\n| Solver verdict on a formalised argument | deterministic; loops reach 100% | ReviewScore, GAAR, DeepA2 |\n| NL→FOL translation correct | 99.0% (207/209, one human expert); 92.7% own-formalisation recognition on synthetic targets; FOL syntax errors 13–38% (2023) | GAAR, DeepA2, LINC |\n| Humans: is one explicit step valid | κ .72 (binary), κ .85 (four-way rubric), α .46 (REVEAL; 18% of chains had a low-agreement step) | SCSearch, METGEN, REVEAL |\n| LLM judging one step (ChatGPT) | 69% balanced with only the cited premises; 52% on the whole chain; wrong steps rejected only 54% of the time; voting does not help rejection | Natural Program |\n| Premise-level vs whole-claim check | κ .18–.40 vs .09–.18 (models vs humans) | ReviewScore |\n| Per-step error compounding | 79% → 18% → ~0% overall-correct from 1 to 3+ steps (T5-11B, strict metric); 58% error-free trees at 82% per-step validity (computed) | EntailmentBank, SCSearch |\n| Agreement between independent reconstructions as a signal | about 10 points above chance (RuleTaker) | DeepA2 |\n\n**Checks with no measured reliability found**\n- Whether the added premise is the right one (author-faithful, plausible). The only numbers are human acceptability and agreement: 45.7% acceptable for gold warrants, κ .18–.31, and a single-rater 89.5% for an LLM faithfulness judge (n unstated).\n- Whether the bridging premise is trivial. There is no automated check with a measured error rate. There is evidence it is a common failure: 56% of fabricated Lean axioms are the conclusion itself, 17% of baseline steps are missing-premise, and GPT-4's rejected warrants were \"if reason then claim\".\n- Cross-model answer agreement as a guarantee about chain steps (SciencePedia): the rate of consensus-but-wrong is unmeasured.\n- Order-invariance of an argument-step check.\n- Whether readers do better when shown an added premise, or whether it makes a weak argument look reasoned.\n- Forced-choice warrant selection as evidence of explication quality: shown to be cue-exploitable on the original ARCT.\n\n**Reading of the evidence (inference, not measured)**\n- Splitting the work into small, narrowly scoped, separately checked tasks does improve measured step quality: 52%→69%, 65%→82%, 38%→70%, and premise-level agreement 2–3 times claim-level.\n- It does not bring those tasks near certainty. Model–human κ stays at .2–.4 for premise factuality and about 69% for balanced step verification. Human–human agreement itself tops out at about .5–.85, depending on how specific the rubric is.\n- The mechanical piece (a solver on a formalisation) is dependable. The content choice (which bridging premise, is it trivial, is it faithful) is where every system either uses an unmeasured LLM judge or a small human rating.\n- The best measured rubric (METGEN, κ .85) names the failure types explicitly, including \"repeats premises\" and \"missing premises\".\n\n---\n\n## What I looked for and did not find\n\n- Any independent critique, replication or citation analysis of SciencePedia in 2026. Semantic Scholar was rate-limited, so its citation list is unseen. OpenAlex showed 0 citing works.\n- SciencePedia's discard rate from cross-model disagreement, any consensus-but-wrong rate, any step-level error rate, any human evaluation of Plato's error rate, the names of the solver models, and the count of QA pairs that survived.\n- Any software implementation or evaluation of Hitchcock's covering-generalization procedure.\n- Any automated check of the non-triviality of a generated bridging premise with a reported accuracy.\n- Any controlled study of showing an AI-inferred implicit premise to people evaluating an argument, and any peer-review-tool user study. ReviewScore measures LLM–human agreement only.\n- Any direct study of a written-in premise making a weak argument look reasoned. Only the adjacent explanation-overreliance studies above.\n- Order-sensitivity measurements for argument-step checks specifically.\n- Error growth with step count for argument explications. Only entailment-tree data, mostly from the T5 era (2021–22), plus one computed extrapolation.\n- Full texts of NLProofS, ReCEval, ROSCOE, LINC, NL2FOL, ChaosNLI, Pavlick & Kwiatkowski, Sanyal et al., ProcessBench, Tyen et al., the Hitchcock 2019 chapter, Hitchcock 2011, and the 2026 Springer implicitness experiment (sample sizes). Those claims rest on abstracts and extracts as tagged.\n- A venue for ReviewScore, GAAR, or Feng & Hunter. None is stated in the versions I read.\n- Betz's Argunauts or syncIALO measuring the quality of the implicit premises themselves. The only metrics reported are syntax, structure and verifiable-reward pass rates.\n"}