自动形式化论证材料推论

自然语言论证在正式明确之前就具有说服力。前提通过文本隐含的可废止的保证、背景承诺和例外条件来支持主张。然而，形式验证则需要相反的情况。要使这些论点可由机器检查，需要构建缺失的承诺，而不仅仅是将给定的句子翻译成逻辑。然而，构造会带来翻译所没有的风险：一个可以自由添加前提的系统可以使任何主张变得可证明，并且正式有效的证明可以直接断言该主张，在没有原始前提的情况下证明它，或者建立比主张本身更多的内容。我们通过将论证材料推理的自动形式化制定为防护完成来解决这个问题，其中非单调材料支持被转化为相对于显式构造的防护集的单调形式推理。仅当其证明既通过了定理证明者又通过了前提依赖性和主张选择性的对比测试时，完成才被接受。我们在 GUARD 中实现了这个公式，这是一个神经符号框架，大语言模型在其中构建和形式化候选守卫，Isabelle/HOL 验证所得理论并返回迭代细化的步骤级反馈，并且当无法忠实完成时系统放弃。我们使用不同 LLM 在 Debatepedia 和 ARCT 上的实证结果表明，与最先进的 LLM 驱动的定理证明方法相比，GUARD 在验证可信性方面取得了显着改进（+35.3，+32.9 点），并大幅减少了泄漏（-25.9，-21.9 点）。此外，我们表明，符号软批评和显式假设层占了大部分收益，软批评还提高了引出上下文的初始有效性，并减少了成功验证所需的迭代次数。