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

• URL: http://arxiv.org/abs/2603.17233v1
• Date: Wed, 18 Mar 2026 00:35:14 GMT
• Title: Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning
• Abstract summary: Auto-formalization (AF) translates natural-language reasoning problems into solver-executable programs.<n>We propose Draft-and-Prune (D&P), an inference-time framework that improves AF-based logical reasoning via diversity and verification.<n>D&P substantially strengthens AF-based reasoning without extra supervision.
• Score: 5.119925615308174
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation [26.089963426404164]
  Autoformalisation systems map natural language reasoning steps into formal statements in a proof assistant such as Lean.<n>Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models.<n>We propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples.
  arXiv  Detail & Related papers  (2026-08-11T13:36:52Z)
• PragReST: Self-Reinforcing Counterfactual Reasoning for Pragmatic Language Understanding [20.011014649243673]
  PragReST is a self-supervised framework that constructs pragmatic QA data.<n>It generates counterfactual reasoning traces and trains models to internalize them.
  arXiv  Detail & Related papers  (2026-06-17T02:41:25Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Stabilizing Efficient Reasoning with Step-Level Advantage Selection [54.563811052329235]
  We show that short-context post-training alone, using standard GRPO without any length-aware objective, already induces substantial reasoning compression.<n>We propose Step-level Advantage Selection (SAS), which operates at the reasoning-step level and assigns a zero advantage to low-confidence steps in correct rollouts and to high-confidence steps in verifier-failed rollouts.
  arXiv  Detail & Related papers  (2026-04-27T03:34:59Z)
• Correct Answers from Sound Reasoning: Verifiable Process Supervision for Language Models [94.68358825189738]
  We propose a post-training framework for verifiable domains that jointly optimize prediction accuracy and reasoning quality.<n>We evaluate VPS on chess, a controlled testbed where reasoning steps can be deterministically verified against engine signals.<n>VPS preserves accuracy while significantly improving reasoning quality, reducing win-rate error by up to 30% and restoring consistency to near saturation.
  arXiv  Detail & Related papers  (2026-04-03T15:19:46Z)
• Learning When to Sample: Confidence-Aware Self-Consistency for Efficient LLM Chain-of-Thought Reasoning [7.8668388431725695]
  Large language models (LLMs) achieve strong reasoning performance through chain-of-thought (CoT) reasoning.<n>Recent self-consistency-based approaches further improve accuracy but require sampling and aggregating multiple reasoning trajectories.<n>This paper introduces a confidence-aware decision framework that analyzes a single completed reasoning trajectory to adaptively select between single-path and multi-path reasoning.
  arXiv  Detail & Related papers  (2026-03-09T22:34:06Z)
• Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
  We propose LogicReward, a reward system that guides model training by enforcing step-level logical correctness with a theorem prover.<n>An 8B model trained on data constructed with LogicReward surpasses GPT-4o and o4-mini by 11.6% and 2% on natural language inference and logical reasoning tasks.
  arXiv  Detail & Related papers  (2025-12-20T03:43:02Z)
• Incorporating Self-Rewriting into Large Language Model Reasoning Reinforcement [54.63337314382886]
  We introduce self-rewriting framework, where a model rewrites its own reasoning texts, and subsequently learns from the rewritten reasoning to improve internal thought process quality.<n>For algorithm design, we propose a selective rewriting approach wherein only "simple" samples, defined by the model's consistent correctness, are rewritten.<n>Experiments on diverse tasks with different model sizes validate the effectiveness of self-rewriting.
  arXiv  Detail & Related papers  (2025-11-20T13:10:52Z)
• Efficient Thought Space Exploration through Strategic Intervention [54.35208611253168]
  We propose a novel Hint-Practice Reasoning (HPR) framework that operationalizes this insight through two synergistic components.<n>The framework's core innovation lies in Distributional Inconsistency Reduction (DIR), which dynamically identifies intervention points.<n> Experiments across arithmetic and commonsense reasoning benchmarks demonstrate HPR's state-of-the-art efficiency-accuracy tradeoffs.
  arXiv  Detail & Related papers  (2025-11-13T07:26:01Z)
• ViFP: A Framework for Visual False Positive Detection to Enhance Reasoning Reliability in VLMs [10.920311878186483]
  We propose ViFP, a framework for Visual False Positive Detection to enhance reasoning reliability in vision-language models.<n>ViFP builds effective reasoning paths through multi-turn QA and dynamically analyzes the consistency of the reasoning path.<n>It also introduces a targeted reasoning chain correction mechanism to modify FP reasoning, thereby improving logical consistency and accuracy.
  arXiv  Detail & Related papers  (2025-08-06T08:31:11Z)
• SEAL: Steerable Reasoning Calibration of Large Language Models for Free [58.931194824519935]
  Large Language Models (LLMs) have demonstrated compelling capabilities for complex reasoning tasks via the extended chain-of-thought (CoT) reasoning mechanism.<n>Recent studies reveal substantial redundancy in the CoT reasoning traces, which negatively impacts model performance.<n>We introduce SEAL, a training-free approach that seamlessly calibrates the CoT process, improving accuracy while demonstrating significant efficiency gains.
  arXiv  Detail & Related papers  (2025-04-07T02:42:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.