Ai system improves formal verification of natural language arguments
Autoformalizing Argumentative Material Inferences
Computation and Language
Summary
Sometimes arguments in natural language sound convincing but don’t show all the assumptions needed to prove them logically. The authors created a system called GUARD that uses AI and formal logic tools to fill in these hidden assumptions carefully, so proofs are trustworthy and precise. GUARD tests its added assumptions by checking whether they are truly necessary to prove the claim and rejects ones that don’t pass these tests. This approach led to big improvements in making formal verifications reliable and avoiding wrong conclusions compared to previous methods.
What this means in practice
- •For legal tech teams: Automatically generate verified formal representations of argument texts to support legal case analysis and verification.$Commercial implications: Enables developing tools that formalize legal arguments with high trustworthiness, improving case preparation and automated reasoning.
- •For debate platform developers: Integrate verified formal argument checking to enhance debate quality and detect unsupported claims in online discussion platforms.
Authors
Xin Quan, Reto Gubelmann, André Freitas
Abstract
Natural language arguments are compelling before they are formally explicit. A premise supports a claim through defeasible warrants, background commitments, and exception conditions that the text leaves implicit. However, formal verification requires the opposite. Making such arguments machine-checkable requires constructing the missing commitments, not only translating given sentences into logic. Construction, however, carries a risk that translation does not: a system free to add premises can make any claim provable, and a formally valid proof may assert the claim outright, prove it without the original premise, or establish more than the claim itself. We address this problem by formulating autoformalization for argumentative material inference as guard completion, in which non-monotonic material support is turned into monotonic formal inference relative to an explicitly constructed guard set. A completion is accepted only when its proof both passes the theorem prover and survives contrastive tests of premise dependence and claim selectivity. We implement this formulation in GUARD, a neuro-symbolic framework in which LLMs construct and formalize candidate guards, Isabelle/HOL verifies the resulting theories and returns step-level feedback for iterative refinement, and the system abstains when no faithful completion can be reached. Our empirical results on Debatepedia and ARCT using different LLMs demonstrate that GUARD yields significant improvements in verified-faithful (+35.3, +32.9 points) and substantial reductions in leakage (-25.9, -21.9 points) over the state-of-the-art LLM-driven theorem proving approach. Moreover, we show that the symbolic soft critique and the explicit assumption layer account for most of these gains, with the soft critique also improving the initial validity of the elicited context and reducing the number of iterations required for successful verification.