论证性实质推理的自动形式化
Autoformalizing Argumentative Material Inferences
- Idiap Research Institute（伊迪亚普研究所）
- University of Zurich（苏黎世大学）
- University of Manchester（曼彻斯特大学）
机构由 AI 辅助整理，请以论文原文为准。
中文总结 AI 辅助
针对论证性实质推理的自动形式化，提出守卫补全方法，通过神经符号框架GUARD将非单调支持转为单调形式推理，经定理证明与对比测试，显著提升验证忠实性并减少泄漏。
中文摘要 AI 辅助
自然语言论证在形式化明确之前就具有说服力。一个前提通过可废止的保证、背景承诺和文本中隐含的例外条件来支持一个主张。然而，形式验证需要相反的做法。使此类论证可机器检查需要构建缺失的承诺，而不仅仅是把给定的句子翻译成逻辑。然而，构建带有翻译所没有的风险：一个可以自由添加前提的系统能使任何主张都可证明，并且一个形式上有效的证明可能直接断言该主张，在不使用原始前提的情况下证明它，或者确立超出主张本身的内容。我们通过将论证性实质推理的自动形式化表述为守卫补全来解决这个问题，在这种补全中，非单调的实质支持相对于一个显式构建的守卫集被转化为单调的形式推理。只有当补全的证明既通过定理证明器，又能在前提依赖性和主张选择性的对比测试中幸存时，该补全才被接受。我们在GUARD中实现了这一表述，这是一个神经符号框架，其中LLM构建并形式化候选守卫，Isabelle/HOL验证所得理论并返回步骤级反馈以进行迭代细化，当无法达到忠实的补全时，系统弃权（不执行）。我们在Debatepedia和ARCT上使用不同LLM的实验结果表明，与最先进的LLM驱动的定理证明方法相比，GUARD在验证忠实性上取得了显著提升（+35.3，+32.9个百分点），并在泄漏上大幅减少（-25.9，-21.9个百分点）。此外，我们表明符号性软批评和显式假设层是这些收益的主要原因，软批评还提高了所引出上下文的初始有效性，并减少了成功验证所需的迭代次数。
英文摘要
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.
