通过多方案生成与验证，提升逻辑推理自动形式化可靠性。
Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning
- 生成多个自然语言计划，基于其生成程序以增强多样性。
- 剔除矛盾或模糊的形式化，用多数投票聚合有效结果。
- 无需额外标注，在多个基准上显著提升准确率，尤其在复杂推理任务中表现优异。
自动形式化（AF）将自然语言推理问题转化为可执行程序，使符号求解器能进行严谨逻辑推导。然而，现有AF流程仍易出错：程序可能无法运行，或运行后语义错误。以往工作主要通过求解器反馈修复语法错误，但语义错误仍是主要瓶颈。本文提出推理时框架Draft-and-Prune（D&P），通过多样性和验证改进基于AF的逻辑推理。D&P首先生成多个自然语言计划，并基于这些计划生成程序；随后剔除可执行但存在矛盾或歧义的形式化，并通过多数投票聚合剩余路径的预测结果。在四个代表性基准（AR-LSAT、ProofWriter、PrOntoQA、LogicalDeduction）上，D&P在无额外监督条件下显著提升性能。在AR-LSAT中，仅使用AF的设置下，GPT-4达到78.43%准确率，GPT-4o达78.00%，远超最强基线MAD-LOGIC与CLOVER。在其余基准上，性能接近上限，包括在PrOntoQA和LogicalDeduction上达到100%。
原文摘要 · Abstract (English)
Auto-formalization (AF) translates natural-language reasoning problems into solver-executable programs, enabling symbolic solvers to perform sound logical deduction. In practice, however, AF pipelines are currently brittle: programs may fail to execute, or execute but encode incorrect semantics. While prior work largely mitigates syntactic failures via repairs based on solver feedback, reducing semantics failures remains a major bottleneck. We propose Draft-and-Prune (D&P), an inference-time framework that improves AF-based logical reasoning via diversity and verification. D&P first drafts multiple natural-language plans and conditions program generation on them. It further prunes executable but contradictory or ambiguous formalizations, and aggregates predictions from surviving paths via majority voting. Across four representative benchmarks (AR-LSAT, ProofWriter, PrOntoQA, LogicalDeduction), D&P substantially strengthens AF-based reasoning without extra supervision. On AR-LSAT, in the AF-only setting, D&P achieves 78.43% accuracy with GPT-4 and 78.00% accuracy with GPT-4o, significantly outperforming the strongest AF baselines MAD-LOGIC and CLOVER. D&P then attains near-ceiling performance on the other benchmarks, including 100% on PrOntoQA and LogicalDeduction.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。