Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning

Abstract

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.

Figures (10)

• Figure 1: End-to-end accuracy ($\mathbf{Acc}$) on four logical reasoning benchmarks. Left: GPT-4 results comparing CoT, Logic-LM, SymbCoT, and D&P. Right: GPT-4o results comparing CoT, SymbCoT, CLOVER, and D&P. "NR" denotes not reported results.
• Figure 2: The algorithmic pipeline of Draft-and-Prune
• Figure 3: A correct Z3Py program corresponds to an input question in AR-LSAT
• Figure 4: Two typical types of ill-defined logical programs which can be detected during inference
• Figure 5: Coverage ($\mathrm{cover}@k$) as a function of the number of sampled AF paths $k$ across four benchmarks.