用来回验证提升大模型形式化文本的准确性
Faithful Autoformalization via Roundtrip Verification and Repair
- 通过双向翻译验证形式化结果是否忠实
- 修复失败案例时定位错误步骤并针对性修正
- 适合法律、规则等高精度形式化场景
当大语言模型将自然语言形式化时，如何确保输出忠实？我们提出一种无需真实标注的往返验证方法：将语句形式化，再翻译回自然语言，重新形式化，并用形式化工具检查逻辑等价性。若两次形式化一致，即表明形式化可信；若不一致，则通过阶段诊断定位错误环节，并使用作用范围受限的修复算子进行修正。我们在德克萨斯州交通法和野生动物法两个法规领域，使用Claude Opus 4.6和GPT-5.2两个模型，结合三种修复基线进行评估。诊断引导的局部修复最有效，其效果依赖诊断函数可靠性。在两个领域和两个模型中，经完整修复系统处理后，未通过等价性检验的规则比通过的规则在NLI漂移上高出1.4倍至2.5倍。
原文摘要 · Abstract (English)
When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural language, re-formalize, and use a formal tool to check logical equivalence. When the two formalizations agree, this provides evidence of a faithful formalization. When they disagree, a stage-level diagnosis localizes the error to a specific translation step, and a scoped repair operator attempts to correct that step. We evaluate the framework on two statutory domains (the Texas Transportation Code and the Texas Parks and Wildlife Code) using two LLMs (Claude Opus~4.6 and GPT-5.2) with three repair baselines. Diagnosis-guided scoped repair is the most effective method, with effectiveness contingent on the reliability of the diagnosis function. Across both domains and both models, under our full repair system, rules that fail the equivalence check show 1.4x-2.5x more NLI drift than rules that pass it.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。