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

TL;DR

Draft-and-Prune enhances auto-formalization for logical reasoning by generating multiple plans, pruning contradictory formalizations, and aggregating results, leading to significant accuracy improvements across benchmarks.

Contribution

It introduces a novel inference-time framework that improves the reliability of auto-formalization through diversity, verification, and majority voting, without requiring extra supervision.

Findings

Achieves 78.43% accuracy on AR-LSAT with GPT-4.

Attains near-ceiling performance on PrOntoQA and LogicalDeduction.

Substantially outperforms previous AF baselines like MAD-LOGIC and CLOVER.

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.