{"path":"research/tools-for-checking-inferences/report-harness-design.md","content":"# Report: designing the model side so it writes checkable single-inference steps\n\n*A research helper's report (Sonnet 5.5, 2026-10-24), saved verbatim on arrival, as it returned it. Brief:\nwhat 2023–2026 research shows about making a model write inferences in a form code can check, skipping what\nour notes already cover (LINC, Logic-LM, SymbCoT, Natural Program, ROSCOE, EntailmentBank, HANS, FOLIO,\nLogicBench). Numbers are the helper's, with its read tags; none was re-checked when this was saved. Home:\n`../tools-for-checking-inferences.md`.*\n\n---\n\n# Research report: designing the LLM side so it writes checkable single-inference steps (2023-2026)\n\nTags: [FULL] = I read the paper pages or results tables; [PART] = read part of the full text, or the full text through a summarising fetch; [ABSTRACT] = abstract or search snippet only; [SECONDARY] = someone else's account. Numbers come from the cited source, never from memory. No paper I found tests your exact form (one rule, one case, kind-named, code-checked), so every lesson below is by transfer. Most results are on 2023-25 models (GPT-4, Gemini 2.5, Llama 3), not on 2026 models.\n\n## A. Compliance with a required form, and what raised it\n\n1. **Let Me Speak Freely?** Tam et al., EMNLP Industry 2024, https://arxiv.org/abs/2408.02442 [PART]. Tested JSON-mode (constrained decoding), format-restricting instructions, and a two-step \"answer in natural language, then convert to the format\". Findings:\n   - Stricter formats lowered reasoning scores.\n   - In 100% of GPT-3.5 JSON-mode answers on Last Letter, the \"answer\" key came before the \"reason\" key, so the model answered directly instead of reasoning first.\n   - Natural-language-then-convert matched unrestricted answers on most models, with occasional conversion errors.\n   - A looser format (\"reply in JSON\") beat a prompt with the full schema on GSM8K.\n   - Lesson: put reasoning fields before verdict fields, and keep thinking separate from form-filling.\n2. **Rebuttal \"Say What You Mean\"**, dottxt, https://blog.dottxt.ai/say-what-you-mean.html [PART, an advocate's blog, not peer-reviewed]. With the same prompt for both arms on Llama-3-8B, structured beat unstructured: GSM8K 0.77 vs 0.78, Last Letter 0.73 vs 0.77. It says Tam's prompts differed between arms. The authors' reply is at github.com/appier-research/structure-gen/blob/main/updates.md. Lesson: the effect is contested and prompt-dependent. Test the form on your own passes, with the same task text in both arms.\n3. **JSONSchemaBench**, Geng et al., 2025, https://arxiv.org/abs/2501.10868 [PART]. About 10K real JSON schemas, six engines, Llama 3.2-1B for the open-source ones. Compliance varies a lot by engine and schema difficulty. Examples from the tables:\n   - GitHub-Hard: Guidance 0.41 empirical coverage, Outlines 0.03, XGrammar 0.28.\n   - Unconstrained LM-only: 0.13 on GitHub-Hard.\n   - Outlines' compliance suffered from timeouts on `minItems`/`maxItems`/`enum`.\n   - Lesson: constrained decoding helps with syntax, but the engine and schema complexity matter. Keep slot schemas flat and simple.\n4. **Grammar-constrained decoding as a logical parser**, Raspanti et al., ACL Industry 2025, https://aclanthology.org/2025.acl-industry.34/ [PART]. 13 open models from 0.5B to 27B, on FOLIO and GSM-symbolic.\n   - On FOLIO, gemma2-2b zero-shot went from 0.02 to 0.21 accuracy with the grammar.\n   - Zero-shot with the grammar often matched or beat 5-shot without it.\n   - Executable rates stayed below 1.0, because semantic errors such as one predicate used with two arities are not caught by a grammar.\n   - Larger models with several shots sometimes lost accuracy under constraint.\n   - Lesson: a grammar guarantees syntax only. The semantic checks have to be your own code.\n5. **LLM+ASP: self-correction with solver feedback**, Ishay & Lee, ACL Findings 2026, https://aclanthology.org/2026.findings-acl.1151/ [FULL, pp. 1-9]. Models were Gemini 2.5 Pro/Flash, o4-mini, DeepSeek R1 and V3, on six benchmarks. The prompt was task-agnostic, with no few-shot examples.\n   - Average accuracy was 54.6% without revision and 78.0% with the self-correction loop (Table 3). The average was 2.18 revisions and 2.3 s.\n   - Syntax errors in final programs fell from 360 without revisions to 18 with them (Table 5).\n   - A compact 2.6k-token reference beat the 22k-token manual: 73.1% vs 70.0% average, and 16 vs 41 syntax errors for reasoning models (Table 2 and text). The authors call this \"context rot\".\n   - The same loop on SMT (the solver language used by Hao et al. 2025) did far worse on nonmonotonic tasks (see C).\n   - The loop's own approval was unreliable. Among accepted outputs, 5.06% (Gemini 2.5 Pro) to 37.33% (DeepSeek V3) were wrong (Table 4).\n   - Unsatisfiable programs gave the solver little to report, while \"wrong answer sets\" gave concrete feedback.\n   - Lesson: an external checker whose error message names the failing field is the strongest compliance lever found. Keep the form spec short. Feedback needs to localise the fault.\n6. **Self-correction needs an outside signal**:\n   - Huang et al., ICLR 2024, https://arxiv.org/abs/2310.01798 [PART]: LLMs cannot self-correct reasoning without external feedback, and accuracy drops after intrinsic self-correction. The apparent gains came from oracle labels.\n   - Olausson et al., ICLR 2024, https://arxiv.org/abs/2306.09896 [PART]: self-repair is bottlenecked by feedback quality. Replacing GPT-4's own explanations with a human's raised repair success from 33.3% to 52.6%.\n   - Lesson: the feedback must come from your code, and the more specific the better. Do not rely on \"check yourself\".\n7. **Hypothesis refinement**, Qiu et al., ICLR 2024, https://arxiv.org/abs/2310.08559 [PART, Table 1 and text]. The model proposes rules, a symbolic interpreter scores them, and feedback goes back.\n   - On ACRE (task accuracy), the best setting (T=3 iterations, N=5 hypotheses) gave 59.0 against 28.0 for plain prompting.\n   - Self-refine with the LM itself as interpreter did much worse.\n   - Lesson: sample a few candidates, filter them with deterministic code, and send back concrete failures.\n\n## B. Step verifiers and premise-linked chains in natural language\n\n8. **PARC**, Mukherjee et al., ICML 2025, https://arxiv.org/abs/2502.02362 [PART; the paper is about math]. The model labels each step with its premises, and each step is checked against only those premises.\n   - Even open-source models reach about 90% recall at identifying premises.\n   - Error identification improves by 6 to 16 points absolute when verifying under premises.\n   - A larger context made models more biased toward \"step is correct\", and the effect was stronger for larger models.\n   - Lesson: have the writer declare premises, and check each step against only its declared premises. This is math, so the transfer is unproven.\n9. **Graph of Verification**, AAAI 2026, https://doi.org/10.1609/aaai.v40i36.40322 [ABSTRACT/excerpt only]. It argues that atomic-granularity, minimal-premise verification relies on premise extraction or declaration that is \"often unreliable\" in loose natural language, and that coarser blocks suit loose text. Lesson: this is the opposing view. Declared premises on a structured form are not extracted premises, so your design tests the form route.\n10. **Process-reward benchmarks outside math**:\n    - LSR-Ben, https://arxiv.org/abs/2605.01203 [ABSTRACT + PART via a summarising fetch; benchmark name differs from an earlier search snippet, so verify]: 3,595 logical and scientific items. Best PRM average 37.4. Best LLM 63.8. Reported false-negative rates are 52.7% for PRMs and 26.6% for LLMs. False-positive rates are 22.7% for PRMs and 28.6% for LLMs.\n    - PRMBench, https://arxiv.org/abs/2501.03124 [PART]: best model 68.8 against human 83.8. Some models scored below random.\n    - Lesson: trained step verifiers are weak outside math. Do not use one as the gate.\n11. **Entailment verification**, Sanyal et al., ACL Findings 2024, https://arxiv.org/abs/2402.03686 [ABSTRACT + PART]. GPT-4 reaches 0.79 macro-F1. LLMs beat humans on multi-hop checks, and humans beat LLMs on one-step deductions such as substitution and negation. Filtering rationales with a fine-tuned verifier added 6% accuracy. Lesson: an LLM verifier is weakest on the simple single-step checks, so those belong to code and form checks.\n12. **LAMBADA**, Kazemi et al., ACL 2023, https://aclanthology.org/2023.acl-long.361/ [PART; 2023, borderline]. Backward chaining as four small few-shot modules (fact check, rule selection, goal decomposition, sign agreement). In a 50-example manual audit at ProofWriter depth 5, CoT had correct proof chains in only 28% of cases where its label was right. Hallucinated facts and rules were the main error. Lesson: one call per sub-step makes each step easier to audit.\n13. Entailer (EMNLP 2022, https://aclanthology.org/2022.emnlp-main.134/, [ABSTRACT]) and NLProofS (EMNLP 2022, [PART]) are before your window, so I mention them only for completeness. The NLProofS verifier raised EntailmentBank proof correctness from 27.7% to 33.3%.\n\n## C. Defeasible and abductive reasoning\n\n14. **BoardgameQA**, Kazemi et al., NeurIPS 2023, https://arxiv.org/abs/2306.07934 [PART]. Few-shot PaLM did poorly at conflict resolution. Tuned models did much better. Proofs were often wrong even when the label was right.\n15. **DEFREASING**, Allaway & McKeown, NAACL 2025, https://doi.org/10.18653/v1/2025.naacl-long.529 [PART]. Twelve LLMs on defeasible reasoning from generics: best overall F1 about 0.64. Strengthening evidence was easier than weakening evidence. Models struggled with irrelevant information.\n16. **Generics and default reasoning**, Kirkpatrick & Sterken 2025, http://arxiv.org/abs/2508.13718 [PART]. Twenty-eight LLMs on 20 patterns. Chain-of-thought lowered accuracy on average by 11.14 points among models above 75% zero-shot. Most models confuse defeasible with deductive inference or read generics as universals. Lesson: the usual-rule kind needs explicit exceptions and external checks.\n17. **MultiLogicNMR and BoardgameQA inside LLM+ASP** (same paper as item 5) [FULL]. On skeptical nonmonotonic tasks, Gemini 2.5 Pro scored 88.5% alone and 100% with ASP. Credulous: 61.0% alone, 93.8% with ASP. The average over models was 90.5 skeptical and 81.0 credulous with ASP, against 59.0 and 52.9 for the baseline LLMs. LLM+SMT was near chance on these, 35.8 and 35.0. BoardgameQA showed no overall gain (82.4% vs 84.7%). The authors flag possible training-data contamination there. Lesson: translating into a formalism that has default and exception built in works.\n18. **Abduction**: the new evidence is about alternatives, not accuracy on a single gold answer.\n    - GEAR, https://arxiv.org/html/2509.24096 [ABSTRACT]: 70B-class models give only about 20% consistent hypotheses. About 80% of equally plausible hypotheses are marked wrong by gold-answer evaluation.\n    - Occam's-razor study, https://arxiv.org/html/2509.03345v2 [ABSTRACT]: models often give valid hypotheses but fail to give the simplest ones. Accuracy falls with complex world models.\n    - HypoBench, https://ar5iv.labs.arxiv.org/html/2504.11524 [ABSTRACT]: the best method recovers 38.8% of ground-truth hypotheses at high difficulty, against 93.8% in base cases.\n    - RECV, https://aclanthology.org/2025.findings-acl.1059.pdf [PART]: error rates of 10-20% for deductive and 32-49% for abductive claim-verification cases, depending on the dataset. Rationales did not always help.\n    - I found no 2024-26 LLM results on alpha-NLI itself (the original ART best was 68.9% vs human 91.4%, 2019 [ABSTRACT]). For your abduction kind, demanding named rivals is untested by these sources. They suggest models do not reliably produce rivals unprompted.\n19. **Deductive vs inductive**: Cheng et al. 2024, https://arxiv.org/abs/2408.00114 [ABSTRACT + PART]. When induction is isolated (the model writes a function and code runs it), GPT-4 scored 1.0 on all their tasks. Deduction, meaning applying a rule to cases, was the weaker step. Lesson: let code, not the model, run the rule where you can.\n\n## D. Inductive rule writing and scope\n\n20. Qiu (item 7) also found, on MiniSCAN, that task accuracy fell from over 80% to almost zero when the same LM applied its own induced rule instead of a symbolic interpreter. Rules were brittle to small changes in the examples. Human-written rules differed in form from LM-written ones.\n21. **Hypothesis Search**, Wang et al., ICLR 2024, https://arxiv.org/abs/2309.05660 [PART]. On 100 ARC problems, GPT-4 with LLM-summarised hypotheses implemented as code reached 30%, against 17% for direct prompting. Human selection from the candidates gave 33%. GPT-4 proposed a correct hypothesis for only 49 of 100 tasks. Lesson: the hypothesis stage is the bottleneck, and code verification is cheap.\n22. I found no 2023-26 paper that directly measures whether LLMs write rules with correct scope and exceptions from cases. GEAR, HypoBench and the Occam paper above are the nearest.\n\n## E. Analogy\n\n23. **SCAR**, Yuan et al., EMNLP Findings 2023, https://aclanthology.org/2023.findings-emnlp.160/ [PART]. Structure abduction means naming the shared structure and mapping the concepts across. GPT-4 reached 65.0% average accuracy, rising to 69.1% with one example plus background knowledge (Table 5). Humans reached 86.0%.\n24. **Targeted-knowledge prompting for proportional analogies**, https://arxiv.org/html/2412.00869v1 [ABSTRACT]. Supplying the specific relation and the cognitive process gave about +21% over no knowledge and about +45% over generic structured knowledge. Best model 55%. Lesson: naming the respect in the prompt helps. I found no study that tests making the model write the respect itself as a rule and then checking it by code.\n25. E-KAR (2022, https://doi.org/10.18653/v1/2022.findings-acl.311 [ABSTRACT]) has the explanation scheme abduce, map, validate. It is before your window and I found no new LLM numbers for it.\n\n## F. Argument mining: implicit premises, schemes, critical questions\n\n26. **CQs-Gen shared task**, ArgMining 2025, https://aclanthology.org/2025.argmining-1.23/ [FULL]. Test set of 34 texts. The top score was 67.6 (ELLIS Alicante), and baselines scored 44.1 and 52.9. Three of the top four teams used scheme annotations. Teams said model choice mattered more than prompt wording. Schemes raised usefulness but cut diversity. Every team that added a classification or ranking step reported gains. Fine-tuning small data did not help much. Dataset label shares: useful 42.7%, unhelpful 31.0%, invalid 26.3% (Table 1).\n27. **Winner**, ELLIS Alicante, https://aclanthology.org/2025.argmining-1.31.pdf [PART]. A questioner generates 8 candidates (half scheme-guided) and a second model picks 3. The LLM selector beat random by only 3.4 points of usefulness, while an oracle beat random by 34.2 points. Lesson: LLM selection adds little over random sampling, and what mattered was generating more candidates.\n28. **TriLLaMA**, https://aclanthology.org/2025.argmining-1.34.pdf [PART]. Classifiers labelled 75-85% of questions \"Useful\" when only 44% were. Debate and deliberation formats did not beat zero-shot. Lesson: LLM judges flatter the writer.\n29. **Argument scheme classification by LLMs**, Bezou-Vrakatseli et al., ACL Findings 2025, https://aclanthology.org/2025.findings-acl.702.pdf [PART]. On real, manually annotated arguments the best result was Claude 3.5 at 0.65 F1 (few-shot with descriptions). Few-shot examples beat formal definitions by about 11 F1 over zero-shot. On automatically generated arguments, scores were near-perfect. Small models were 40-50 points lower. Cause-to-effect was the most confused scheme. Lesson: kind labelling is uncertain on real text, so do not let the writer's own label be the final authority.\n30. **Toulmin explication**, Gupta et al., ACL 2024, https://aclanthology.org/2024.acl-long.552/ [PART, pp. 4-9]. Prompting \"According to Toulmin model\" gave a complete claim/grounds/warrant breakdown 99-100% of the time for GPT-4 (Table 1). In a human study with 300 judgments per type, warrants were acceptable in 61.7% for GPT-4, 45.7% for the datasets' gold warrants and 26.3% for Llama-2-70B. Judges rejected warrants that restated the claim or \"if reason then claim\". Agreement between annotators was low (kappa 0.18 on gold, 0.24 on GPT-4). Lesson: form compliance is easy, but substance is subjective. Require a check that a warrant is more than a restatement.\n31. **Enthymeme reconstruction**: Delas et al. 2024, https://doi.org/10.3233/faia240310 [PART]: scheme classification macro-F1 0.93, argument validation 0.77, against 0.51 for the no-scheme baseline. Sviridova et al., CMNA 2025, https://ebooks.iospress.nl/volumearticle/80520 [ABSTRACT]: human experts often could not tell LLM reconstructions from human ones. No numbers in the abstract.\n\n## G. LLM as translator into a symbolic engine\n\n32. **QUITE**, Schrader et al., EMNLP 2024, https://doi.org/10.18653/v1/2024.emnlp-main.153 [PART]. GPT-4 prompted to write ProbLog had about 76% parsing errors. A fine-tuned Mistral-7B text-to-ProbLog parser was the only approach that answered about half the questions correctly. Lesson: prompting alone is poor for strict-syntax targets, and fine-tuning or constrained decoding is needed.\n33. **Lightweight LLMs for ASP**, CEUR Vol-4270 short6 / LPNMR 2026 [PART]. Best fine-tuned model: 99.0% syntactic accuracy for one model, 82.0% semantic accuracy for another. The best syntax model had only 55.0% semantic accuracy. Lesson: syntax success and meaning-preserving translation are different numbers.\n34. **Logic of Thought**, https://arxiv.org/html/2505.16114v1 [ABSTRACT + table]: near-perfect puzzle accuracy for GPT-4o with ASP (e.g. 100% on Sudoku, Hitori, Fillomino). Ishay et al., KR 2023, https://doi.org/10.24963/kr.2023/37 [ABSTRACT]: most errors were simple enough for humans to fix.\n\n## Gaps found\n\n- No paper on writing one-inference steps against a form with a deterministic check, and no measurement of compliance rates for \"one rule per step\". Your own few-percent figure stays the only direct number.\n- No new 2024-26 LLM numbers for delta-NLI, alpha-NLI or E-KAR.\n- No paper measures LLM-written rules for correct exceptions from cases.\n- Most PRM, premise-link and ASP evidence is math, puzzles or synthetic. The argument-mining evidence is closest to your domain and weakest on method.\n\n## The five design moves best supported by evidence, ranked\n\n1. **Code checks the form and sends specific error messages back for a few revisions.** Ishay & Lee (ACL Findings 2026) went from 54.6% to 78.0% with solver feedback and cut syntax errors from 360 to 18. Huang et al. and Olausson et al. show it fails without an outside signal and with weak feedback.\n2. **Free reasoning first, then fill the slots, with reasoning fields before verdict fields.** Tam et al. found answer-before-reason ordering collapsed reasoning and that natural-language-then-convert held up. Constrained decoding is only a syntax guarantee (Raspanti: executable rate below 1.0). The dottxt rebuttal means this effect needs a same-prompt test on your passes.\n3. **The writer declares the step's premises by id, and each step is checked against only those premises, one call per step.** PARC (premise-linked verification: +6 to 16 points, about 90% premise recall) and LAMBADA (per-module calls; CoT chains correct in only 28% of audited cases) support it. Graph of Verification warns that this is fragile in loose language, so measure it.\n4. **Sample a few candidates and filter them with deterministic checks. Do not use an LLM judge as the gate.** Hypothesis refinement used an interpreter's score. LLM selection added only 3.4 points over random in the CQs-Gen winner, TriLLaMA's judges called 75-85% of questions useful when 44% were, and LLM+ASP's own verifier let through 5-37% wrong outputs.\n5. **Per-kind slot templates, kept short, with one or two worked examples each, and for \"usually\" rules a mandatory exceptions slot plus a separate call that applies the rule to the case.** Bezou-Vrakatseli found few-shot examples beat definitions by about 11 F1, LLM+ASP found a 2.6k-token reference beat a 22k-token one, Kirkpatrick and DEFREASING found models treat generics as universals or confuse defeasible with deductive inference, and Qiu found models apply their own rules poorly.\n"}