Autoformalizing Argumentative Material Inferences

• Natural-language arguments rely on implicit warrants, shared commitments, and unstated exceptions, so verification requires making their support explicit.Material inference can be defeasible, with conclusions withdrawn when exceptions or counterarguments arise.Source: Introduction · p. 1
• Because constructing missing commitments can make almost any claim provable, formal validity alone cannot ensure that a proof preserves the original support.Faithful verification must also test premise dependence and claim selectivity, since a guard can state the answer, weaken the target, or make the premise irrelevant.Source: Introduction · p. 2
• GUARD builds context from assumptions, definitions, and exceptions, formalizes defeasible rules with explicit abnormality guards, and uses LLM critique and Isabelle/HOL feedback for refinement.It accepts a proof only when replacing the premise or claim with alternatives that should not support the inference makes the perturbed theory unprovable.Source: Introduction · p. 2
• GUARD improves average verified-faithful rate over the strongest baseline by 35.3 points on Debatepedia and 32.9 points on ARCT, while reducing leakage by 25.9 and 21.9 points, respectively.The evaluation used GPT-5.1, Qwen3-Max, DeepSeek-V3.2, and Mistral Medium 3.5 as backbone LLMs.Source: Introduction · p. 2
• Removing soft symbolic critique or the assumption layer lowers verified-faithful rate by up to 40.5 and 31.5 points, respectively, and 63.5 to 74.3 percent of abstentions trace to missing guards.The diagnostic analysis attributes residual leakage to premise-side failures.Source: Introduction · p. 2

Problem Definition

• The goal is to construct a strengthened context and guards whose combination with premise T formally entails claim C.The guards are a subset of the strengthened context Γ↑, and G ∪ {T} |= C must hold.Source: Problem Definition · p. 2
• The system formalizes the premise, claim, and guards, then asks an external theorem prover to prove the claim from the premise and guard axioms.The theory uses the formalized premise as an assumption, the claim as the goal, and formalized guards as axioms.Source: Problem Definition · p. 2
• When proof fails, a refinement controller uses failed proof steps to update the guard set until proof succeeds or the refinement budget is exhausted.The controller iteratively generates refined guard sets.Source: Problem Definition · p. 2

Stage I: Context Strengthening

• Stage I constructs a strengthened context from assumptions, normalized definitions, and exception-aware defeasible rules, then selects step-specific guards from that context.Assumptions are linked to the premise–claim edge they support; exceptions specify when local rules are blocked.Source: Stage I: Context Strengthening · p. 3

Stage II: Soft Verification and Refinement

• Stage II maps context sentences into first-order logical forms aligned with Isabelle/HOL, converts assumptions and definitions into axioms, and encodes exceptions as guarded rules.The translation uses Neo-Davidsonian event semantics to keep predicate–argument structure close to the sentence while preserving its information content.Source: Stage II: Soft Verification and… · p. 3
• An LLM critic selects guards and checks representation correctness, support adequacy, strict entailment, and dependence on both the premise and every guard.The dependence checks require that the guards alone do not prove the claim and that removing any selected guard prevents the proof.Source: Stage II: Soft Verification and… · p. 4

Stage III: Hard Verification and Refinement

• Stage III encodes selected guards as Isabelle/HOL axioms and the premise and claim as the theorem’s assumption and goal; failed proof steps guide iterative hard refinement.Refinement can correct formal representations or context, update guard selection when needed, and recheck the theory.Source: Stage III: Hard Verification and… · p. 4

Stage IV: Faithfulness Check

• Stage IV tests premise sensitivity by substituting empty or counter-premises and claim selectivity by substituting nearby unwarranted claims; a candidate passes only if none remains provable.Faithfulness refinement addresses leaks by conditioning unconditional claim assertions or narrowing over-broad guards while preserving the original entailment, for up to five iterations; outputs distinguish verified-faithful, reject-leaky, and two abstention outcomes.Source: Stage IV: Faithfulness Check · p. 4

Datasets and Models

• The evaluation uses 247 balanced Debatepedia pairs (13 per topic across 19 topics) and 200 randomly sampled ARCT reason–claim pairs treated as premise–claim pairs.ARCT examples require an implicit warrant to connect reason and claim.Source: Experimental Setup · p. 5
• The framework was tested with GPT-5.1, Qwen3-Max, DeepSeek-V3.2, and Mistral Medium 3.5, using Isabelle/HOL as the logical solver.Source: Experimental Setup · p. 5

Baselines

• Four baselines are direct autoformalisation, 1-shot CoT, Toulmin-style 1-shot explication, and PEIRCE; PEIRCE and GUARD use a 10-iteration maximum.The CoT baseline uses one in-context example (Wei et al. 2022; Wang et al. 2023); Toulmin-style explication follows Gupta, Zuckerman, and O’Connor (2024), and PEIRCE follows Quan et al. (2025a).Source: Experimental Setup · p. 5

Results and Evaluation

• 61.13 VFR on Debatepedia and 65.00 on ARCT put GUARD 35.3 and 32.9 points above PEIRCE, with the highest SP and VFR for every backbone and dataset.GUARD converges within 3.13 to 3.85 hard iterations on average; Direct achieves a 0.00 solver-pass rate under all four backbones on both datasets.Source: Results and Evaluation · p. 6
• 4.06% and 2.72% leakage for GUARD contrast with PEIRCE’s 29.96% and 24.64%, as PEIRCE’s leaked candidates mostly bypass the premise rather than contradict it.PEIRCE’s empty-premise failure rates are 25.03% and 22.36%, versus counter-only rates of 0.53% and 0.00%; GUARD blocks this path through dependence obligation PO4 and an empty-premise probe.Source: Results and Evaluation · p. 6, Table 2 · p. 6
• 35.0% and 36.0% of GUARD’s first theories are valid on Debatepedia and ARCT, versus 25.0% and 26.1% for PEIRCE; hard refinement adds 28.6 and 30.8 points versus 11.6 and 16.4.Symbolic critique checks guard logical forms against four proof obligations before Isabelle/HOL, repairing malformed representations, missing support, and padded guards.Source: Results and Evaluation · p. 6, Figure 2 · p. 6
• 3.6 to 9.0 assumptions and 5.8 to 8.5 definitions accumulate during the first five soft iterations on Debatepedia, while exceptions grow more gradually throughout refinement.After five iterations, assumption and definition counts flatten; ten hard iterations add at most 0.9 assumptions and 0.5 definitions or exceptions per instance, indicating local guard corrections.Source: Results and Evaluation · pp. 6–7, Figure 3 · p. 7
• 40.5 and 39.5 points of VFR are lost without soft critique, while removing assumptions costs 23.5 and 31.5 points on Debatepedia and ARCT, respectively.Without soft critique, leakage rises to 24.58% and 21.70%; definitions cost a further 14.2 and 9.5 points, and exceptions 2.8 and 2.5 points.Source: Results and Evaluation · p. 7, Table 3 · p. 7
• 63.5–74.3% of unproven instances are abstain-missing-guards, and a doubled budget raises GPT-5.1 solver-pass rates to 93.5% on Debatepedia and 95.5% on ARCT.The remaining abstain-not-compatible cases range from 6.5% to 16.6% on Debatepedia and 4.5% to 14.0% on ARCT, contracting as the backbone strengthens.Source: Results and Evaluation · p. 7, Figure 4 · p. 7

Material inference, defeasibility, and implicit warrants

• GUARD builds on inferentialist material inference, non-monotonic reasoning, and NLP work reconstructing implicit warrants, operationalizing these ideas as an autoformalization problem with explicit success and failure states.The cited foundations include Brandom (1994, 2008, 2002), Hlobil and Brandom (2024), Reiter (1980), McCarthy (1980), Pollock (1987), Dung (1995), Habernal et al. (2018), and Gupta, Zuckerman, and O’Connor (2024).Source: Related Work · p. 7

Argument mining, debate corpora, and support structure

• Unlike debate-corpus studies that predict labels, retrieve support, or reconstruct warrants in natural language, GUARD starts from a given support relation and constructs a proof package exposing its hidden bridge without changing meaning.Prior work studies argumentative support, contradiction, and structure in Debatepedia and related corpora (Niculae, Park, and Cardie 2017; Lawrence and Reed 2020).Source: Related Work · p. 7

Closest work: solver-guided explanation verification

• Unlike solver-guided explanation verification for NLI, which refines given explanations, GUARD searches for admissible guards for debate premise-claim pairs and requires solver validity plus contrastive faithfulness.The cited NLI work is Quan et al. (2024b, 2025a).Source: Related Work · pp. 7–8

Conclusion

• GUARD consistently outperforms state-of-the-art LLM-driven theorem proving on Debatepedia and ARCT across four backbone LLMs.Source: Conclusion · p. 8
• GUARD formulates autoformalization of argumentative material inference as guard completion.Source: Conclusion · p. 8
• Guard completion turns implicit, non-monotonic support into explicit, deductively checkable inference.Source: Conclusion · p. 8
• GUARD combines context strengthening, symbolic soft critique, and solver-guided hard refinement.Source: Conclusion · p. 8
• GUARD also uses contrastive faithfulness checks.Source: Conclusion · p. 8
• Future work will extend guard completion to material inferences from a broader range of domains.Source: Conclusion · p. 8

A.1 Datasets and Sampling

• The evaluation uses 247 Debatepedia premise–claim pairs and 200 randomly sampled ARCT reason–claim pairs, with the same instances used for every method and backbone.Debatepedia pairs are balanced across 19 topics, with 13 pairs per topic.Source: §A.1 · p. 9
• Debatepedia tests whether implicit contextual commitments can make material argumentative support formally verifiable, rather than treating support as textual entailment.Its 13 pairs per topic give each of the 19 topics equal weight, without assuming equal reasoning difficulty.Source: §A.1 · pp. 9–10
• ARCT focuses on implicit warrants, but this evaluation uses reason–claim pairs for guard completion and does not score the original warrant-selection task (Habernal et al. 2018).Success is assessed through the resulting proof and contrastive checks.Source: §A.1 · p. 10

A.2 Backbone LLMs and Inference Settings

• The framework is evaluated with GPT-5.1, Qwen3-Max, DeepSeek-V3.2, and Mistral Medium 3.5 through their respective APIs.The four models span distinct families, enabling cross-family comparisons without establishing an exhaustive ranking of available LLMs.Source: §A.2 · p. 10
• For GPT-5.1, reasoning_effort is medium; Qwen3-Max and DeepSeek-V3.2 use non-thinking mode, and temperature=0.6 is set for those models and Mistral Medium 3.5.No sampling temperature is specified for GPT-5.1, and reasoning_effort is not explicitly set for Mistral Medium 3.5.Source: §A.2 · p. 10
• Methods sharing a task use identical decoding configurations within each backbone, and each example is prompted independently without cross-backbone demonstrations.The reported model identifiers are gpt-5.1, qwen3-max-preview, deepseek-chat, and mistral-medium-3-5.Source: §A.2 · p. 10
• Repeating same-model method comparisons across backbones tests whether guard completion’s contribution persists as the underlying LLM changes.The selection is not exhaustive; evaluating other general-purpose backbones or additional versions within one family could extend the comparison.Source: §A.2 · p. 10

A.3 Baseline Control Conditions

• All methods use the same autoformalisation and Isabelle/HOL pipeline, and solver-passed candidates undergo shared premise-contrast and claim-contrast tests.Methods differ only in how they produce missing inferential material and whether they revise it iteratively.Source: §A.3 · p. 10
• Direct autoformalisation supplies no added context, while one-shot CoT and Toulmin baselines test general background reasoning against an explicit warrant-and-qualification schema.Toulmin-style context also relates the warrant to supporting background information and expresses circumstances under which support applies.Source: §A.3 · pp. 10–11
• PEIRCE provides an iterative neuro-symbolic comparison whose explanatory context can be refined using theorem-prover feedback, within a shared 10-iteration limit.This aligns the hard-refinement budget between PEIRCE and GUARD. (Quan et al. 2025a)Source: §A.3 · p. 11

B.1 Representation Language

• Natural-language sentences are represented with Neo-Davidsonian event variables, participant-role predicates, scoped quantifiers, and consistent predicates, polarity, and connectives.Distinct verbal eventualities receive distinct event variables.Source: §B.1 · p. 11
• The autoformaliser parses constituents, maps them to logical forms, and unifies predicates across the instance; selected guards become axioms, the premise an assumption, and the claim the proof goal.Unification uses a shared predicate signature so each concept has the same symbol and arity throughout the instance.Source: §B.1 · p. 11

B.2 Formalisation of Exception-Management Items

• Defeasible rules become monotonic guarded rules using abnormality predicates, with open exception lists asserting only that listed exceptions imply abnormality.This avoids claiming that an open-ended elicited exception list is exhaustive; abnormality conditions are defined differently for closed lists.Source: §B.2 · p. 11

B.3 Automatic Quality Checks

• Logical forms are checked for syntax, variable binding, predicate consistency, semantic coverage, role fidelity, and inference direction before entering a theory.Checks preserve source content, modifiers, polarity, connectives, event-participant roles, and the direction of implications, causal links, and defeasible rules.Source: §B.3 · p. 12

B.4 Faithfulness Evaluation of Autoformalisation

• Informalisation compares each logical form’s natural-language rendering with its source by sentence-embedding cosine similarity, while human review categorizes errors as syntax, implication, quantifier, or variable.The evaluation covers premise, claim, and guard sentences.Source: §B.4 · p. 12
• Because all compared methods share the autoformalization component, its errors affect every system equally.Source: §B.4 · p. 12
• Faithfulness is high and stable across backbones (0.798–0.917), while errors concentrate on syntax and semantic errors form a minority.The syntactic admission check detects and repairs the dominant syntax errors before verification.Source: §B.4 · p. 12, Table B.1 · p. 12, Figure B.1 · p. 12

C.1 Theory Construction

• The Isabelle/HOL theory declares entity and event types and unified predicates, inserts selected guards as named axioms, and sets the formal premise as an assumption and claim as the goal.A proof succeeds only when Isabelle/HOL establishes the goal.Source: §C.1 · p. 12
• Before proof search, a syntax check runs the theory through Isabelle and returns parser or type-checker errors and affected lines for bounded LLM refinement.Source: §C.1 · p. 13
• A consistency check asks Sledgehammer to prove False; contradictory axiom sets are rejected, with contradiction-supporting axioms returned for refinement, and only theories passing both checks proceed.Source: §C.1 · p. 13

C.2 Proof Search with Sledgehammer

• Direct Sledgehammer searches from the premise and guard axioms; Isabelle rechecks any reconstructed tactic before the theory is counted as solver-passed.The proof line in Listing C.1 was obtained in direct mode.Source: §C.2 · p. 13
• If direct search fails, an LLM sketches an Isar proof with guard-dependent intermediate facts; each ATP placeholder must be discharged before Isabelle rechecks the whole proof.A failed step, preceding comments, and prover messages become failure context; explicit decomposition can help multi-guard instances.Source: §C.2 · p. 13

C.3 Failure Extraction and Hard Refinement

• On failure, the controller records the failing theorem or step, goal state, relevant diagnostics, prover messages, and supplied axioms for hard refinement.The refinement function classifies failures under PO1–PO4, may correct representations or add or refine missing context, and can change guard selection while leaving the original premise and claim unchanged.Source: §C.3 · p. 14

D Prompt Templates

• Baseline templates cover chain-of-thought background context, explanatory-sentence generation, and Toulmin-style context generation.The templates are followed by pipeline-stage prompts; placeholders are instantiated at run time, and the complete prompts and demonstrations are in the submitted code.Source: Table D.1 · p. 14, Table D.2 · p. 14, Table D.3 · p. 14
• Pipeline templates elicit enthymematic assumptions, definitions and term-normalisation facts, defeasible rules and exceptions, and logical forms.Definition prompts preserve context-specific meanings and prohibit broadening terms or introducing claim-bearing definitions; translation prompts require only sentence-licensed content and compilable logical forms.Source: Table D.5 · p. 15, Table D.6 · p. 15, D Prompt Templates · pp. 15–16
• The guard-selection prompt asks for the smallest supplied guard set that jointly covers missing inferential material, without inventing an item.The prompt templates also include soft symbolic critique, Isabelle-diagnostic refinement, and premise- and claim-side contrastive probes.Source: D Prompt Templates · p. 16, Table D.8 · p. 16, Table D.9 · p. 16
• The leakage-repair prompt requires revised guards to preserve the original proof while blocking guard-only, counter-premise, and alternative-claim proofs, with every guard justified and load-bearing.It directs the model to narrow or condition over-broad rules rather than add unrelated blockers.Source: D Prompt Templates · p. 17, Table D.12 · p. 17

E Complete Ablation Results

• Removing soft critique is the single most damaging intervention across all four backbones.Source: E Complete Ablation Results · p. 17
• The contribution ordering A ≻ ∆ ≻ X remains stable across backbones and datasets.Source: E Complete Ablation Results · p. 17
• Table E.1 reports the ablation for every backbone on both datasets, beyond the GPT-5.1 ablation reported in the main paper.Source: E Complete Ablation Results · p. 17

F End-to-End Example

• The end-to-end example follows Debatepedia instance #197 from context harvesting through the selected guards’ autoformalisation.Source: F End-to-End Example · p. 17
• The instance trace records soft and hard verification together with their refinements.Source: F End-to-End Example · p. 17
• The example concludes with contrastive checks.Source: F End-to-End Example · p. 17

F.1 Debatepedia #197: Video-Game Play and Cognitive Benefits

• The selector chose three initial guards: G1 maps positive effects to cognitive benefits, G2 aligns developing minds with young people, and G3 licenses the inference subject to an exception for effects that are too rare, small, or fragile.G3 is the defeasible rule that moves from potential positive cognitive effects to saying an activity can have cognitive benefits for young people.Source: §F.1 · p. 18
• A strict-support failure added G4–G7 to connect developing minds to young people, supply the default rule’s antecedent, exclude its exception, and carry the conclusion from play to video games.G4–G7 were added during the soft verification–refinement loop.Source: §F.1 · pp. 18–19
• Hard prover feedback added G8, which transfers a cognitive benefit from a young person’s mind to that young person.The failed proof step required a guard licensing that transfer.Source: §F.1 · p. 19
• The original theorem is provable, while the empty-premise, harm-focused counter-premise, and excessive-play alternative-claim probes are unprovable, making the instance Verified-Faithful.The checks show that the guards do not entail the claim without the premise, license it from a harm-focused premise, or extend the moderate-play premise to excessive play.Source: §F.1 · pp. 20–21