Draft-and-Prune：提升面向逻辑推理的自动形式化可靠性

自动形式化（AF）将自然语言推理问题翻译为求解器可执行的程序，使符号求解器能够进行可靠的逻辑演绎。然而在实践中，现有 AF 流水线很脆弱：程序可能无法执行，或者虽能执行却编码了错误语义。尽管已有工作通过基于求解器反馈的修复在很大程度上缓解了句法失败，减少语义失败仍是主要瓶颈。我们提出 Draft-and-Prune（D&P），一个通过多样性与验证来改进基于 AF 的逻辑推理的推理时框架。D&P 首先起草多个自然语言计划，并以这些计划为条件进行程序生成。它进一步剪除可执行但矛盾或含糊的形式化结果，并通过多数投票聚合幸存路径的预测。在四个代表性基准（AR-LSAT、ProofWriter、PrOntoQA、LogicalDeduction）上，D&P 无需额外监督即大幅增强基于 AF 的推理。在 AR-LSAT 的纯 AF 设定下，D&P 以 GPT-4 达到 78.43% 准确率、以 GPT-4o 达到 78.00% 准确率，显著超越最强 AF 基线 MAD-LOGIC 与 CLOVER。D&P 在其他基准上接近满分，包括在 PrOntoQA 与 LogicalDeduction 上达到 100%。