Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.17233 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914425784500224 |
|---|---|
| author | Ni, Zhiyu Liang, Zheng Song, Liangcheng Cao, Chenrui Zhang, Xian Sangiovanni-Vincentelli, Alberto Nuzzo, Pierluigi |
| author_facet | Ni, Zhiyu Liang, Zheng Song, Liangcheng Cao, Chenrui Zhang, Xian Sangiovanni-Vincentelli, Alberto Nuzzo, Pierluigi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_17233 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning Ni, Zhiyu Liang, Zheng Song, Liangcheng Cao, Chenrui Zhang, Xian Sangiovanni-Vincentelli, Alberto Nuzzo, Pierluigi Artificial Intelligence 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. |
| title | Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2603.17233 |