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 & tables
Figure 1: End-to-end accuracy ( 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
Paradigm
Method
Fallback
LLM
End-to-end Accuracy (%)
Policy
AR-LSAT
ProofWriter
PrOntoQA
LogicalDeduction
Prompting
Direct
N/A
GPT-4
33.30
52.67
77.40
71.33
CoT
35.06
68.11
91.00
74.67
CoT-SC
–
69.33
93.40
74.67
DetermLR
–
79.17
98.60
85.00
SymbCoT
43.91
82.50
99.60
93.00
Table 1: End-to-end accuracy ( Acc ) on four deductive reasoning benchmarks. We compare prompting-based methods and auto-formalization (AF) methods, without fallback (abstention) and with CoT fallback. “–” indicates that the corresponding setting is not supported by the baseline.
Method
LLM
Acc (%)
ExecRate (%)
Acc (%) @Exec
Logic-LM
GPT-4
19.6
32.6
60.0
D&P ( k=1 )
36.4
43.3
84.1
D&P ( k=20 )
78.4
91.7
85.5
CLOVER
GPT-4o
46.8
59.7
78.3
D&P ( k=1 )
39.9
44.6
89.4
D&P ( k=20 )
78.0
89.6
87.1
Table 2: Decomposed AF diagnostic metrics on AR-LSAT. k denotes the number of sampled AF paths.
Figure 5: Coverage ( cover@k ) as a function of the number of sampled AF paths k across four benchmarks.
AccAF (%)
AF w/o draft
AF w/ draft
AR-LSAT
36.35 ± 1.22
41.78 ± 2.46
ProofWriter
97.69 ± 0.18
98.33 ± 0.22
PrOntoQA
94.92 ± 0.84
99.56 ± 0.18
LogicalDeduction
98.60 ± 0.58
98.23 ± 0.32
Table 3: Accuracy with a naive AF path w/ and w/o drafted plans (on GPT-4, w/o pruning).
Figure 6: Diagnostic metrics on ProofWriter across different numbers of paths ( k ).
Figure 7: AccAF on AR-LSAT w/o vs. w/ pruning across different numbers of paths ( k ). Without pruning, the AccAF plateaus around 45% quickly, while pruning enables further accuracy boost to around 78% .
AccAF (%)
w/o Pruning
w/ Pruning
AR-LSAT
45.13 ± 0.34
78.43 ± 0.55
ProofWriter
98.33 ± 0.00
98.33 ± 0.00
PrOntoQA
99.34 ± 0.10
99.32 ± 0.10
LogicalDeduction
99.33 ± 0.00
99.50 ± 0.18
Table 4: The AccAF (%) of D&P w/o vs. w/ pruning on four benchmarks. There are twenty paths ( k=20 ), and every path uses drafted plans.
Figure 8: Diagnostic metrics on AR-LSAT w/o vs. w/ pruning across different numbers of paths ( k ).
Appendix figures & tables14 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 9: AF-only accuracy versus k for D&P without pruning and D&P with pruning on AR-LSAT.
Figure 10: Accuracy versus path budget k for CoT-SC and D&P on on AR-LSAT.
Model
Method
Acc (%)
ExecRate (%)
Acc@Exec (%)
Coverage@k (%)
DeepSeek-R1
CoT
83.04
100.00
83.04
83.04
DeepSeek-R1
D&P
93.83
99.52
94.28
95.96
GLM-4-plus
CoT
49.13
100.00
49.13
49.13
GLM-4-plus
D&P
80.00
93.04
85.98
86.96
Kimi-K2.5
CoT
95.65
100.00
95.65
95.65
Kimi-K2.5
D&P
95.43
99.13
96.27
95.65
Appendix
Table 5: Generalization to additional backbones on AR-LSAT ( k=10 used for D&P, and 3-shot used for CoT).
k
LINC ( T=0 )
LINC ( T=1 )
D&P
1
38.22
38.17
39.87
5
39.30
44.09
64.04
10
39.65
44.65
72.17
15
40.30
44.52
75.91
20
40.61
44.57
78.00
Appendix
Table 6: LINC-style proxy vs. D&P on AR-LSAT (GPT-4o).
k
LINC
D&P
1
98.92
98.60
5
99.92
99.43
10
100.00
99.50
15
100.00
99.63
20
100.00
99.67
Appendix
Table 7: LINC-style proxy vs. D&P on ProofWriter (GPT-4o).
Model
Majority vote (%)
Solver-weighted vote (%)
GPT-4o
78.00
81.74
GPT-5.2
93.91
94.35
Gemini-3-flash
95.65
95.65
Appendix
Table 8: Majority vs. solver-weighted aggregation on AR-LSAT ( k=20 ).
TDRAFT
0.0
0.5
1.0
1.1
1.2
1.3
Acc@k20 (%)
60.17
71.87
78.00
75.83
75.65
70.87
Appendix
Table 9: Drafting temperature ablation on AR-LSAT with GPT-4o (Acc@k20).
ICL
Acc@k20
Avg input tokens/path
Avg output tokens/path
Avg total tokens/path
0
55.30
1,555
1,574
3,129
1
65.65
2,684
1,199
3,883
3
78.00
5,200
1,057
6,257
5
78.61
8,817
1,078
9,895
Appendix
Table 10: ICL shot ablation on AR-LSAT (GPT-4o, k=20 ).
max_repairs
Acc (%)
ExecRate (%)
Acc@Exec (%)
0
36.09
87.83
41.09
1
40.00
96.52
41.44
2
45.65
97.39
46.88
3
36.52
97.83
37.33
Appendix
Table 11: Effect of maximum repair rounds on AR-LSAT (GPT-4o, k=1 ).
Category
Count
% Fail
% All
Coverage failure A
19
37.25
8.26
Coverage failure B
16
31.37
6.96
Aggregation failure
16
31.37
6.96
Appendix
Table 12: Failure taxonomy on AR-LSAT ( k=20 , with pruning, GPT-4).
Category
Count
% Fail
% All
Coverage failure A
24
48.00
10.43
Coverage failure B
13
26.00
5.65
Aggregation failure
13
26.00
5.65
Appendix
Table 13: Failure taxonomy on AR-LSAT ( k=20 , with pruning, GPT-4o).
CoT-SC
D&P
k
Acc@k
Tokens
Acc@k
Tokens
1
34.09
2,008
39.87
6,257
5
36.78
10,040
64.04
31,283
10
37.70
20,081
72.17
62,567
15
38.52
30,121
75.91
93,850
20
38.35
40,162
78.00
125,134
Appendix
Table 14: Cost-normalized comparison on AR-LSAT (GPT-4o).
Benchmark
Solver
GPT-4o
GPT-4
AR-LSAT
Z3Py
1 / 4600
2 / 4600
ProofWriter
PyKe
0 / 12000
0 / 12000
PrOntoQA
PyKe
0 / 10000
0 / 10000
LogicalDeduction
CSP
0 / 6000
4 / 6000
Appendix
Table 15: Path-level timeout statistics under k=20 .
TDRAFT
Acc@k20 (%)
PathAcc (%)
HitRate@k20 (%)
Havgnorm
0.0
60.17
39.43
61.30
0.026
0.5
71.87
39.17
75.65
0.049
1.0
78.00
39.13
83.91
0.068
1.1
75.83
38.30
82.17
0.076
1.2
75.65
36.96
80.43
0.096
1.3
70.87
34.10
76.42
0.102
Appendix
Table 16: Answer distribution statistics vs. drafting temperature on AR-LSAT (GPT-4o, k=20 ; entropy computed on valid single-label paths).
Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models, which come with limited guarantees of accuracy. In addition, these methods typically only consider inputs that are known to be correct, and therefore do not assess whether the AF translates incorrect inputs faithfully. To address these limitations, we propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples. Our method is based on automatically generating perturbed reasoning steps that are designed to be invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. We apply our method to eight AF systems across four mathematical datasets, and observe pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements. The most validity-preserving fine-tuned AFs are also the most sycophantic, suggesting a tension between validity and invalidity preservation in current AF systems.
Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh +7
Nanyang Technological University, Singapore · University of Oxford, United Kingdom · The University of Edinburgh, United Kingdom
Frontier reasoning-tuned language models still fail on deductive tasks at depth, and the cost of improved performance through extended internal reasoning scales poorly. Symbolic delegation offers a complementary route: a language model translates the problem, while a solver performs the inference. However, current autoformalization pipelines for logic programming are typically bespoke integrations tied to particular tasks or agents. We introduce PrologMCP, a task-agnostic, open-source server that exposes Prolog as a stateful tool through the Model Context Protocol (MCP). Its compact tool interface, structured error reporting, and per-session isolation make the translate-run-inspect-repair loop a reusable primitive for MCP-capable agents. We evaluate a formalizer agent enhanced with PrologMCP against standard and reasoning LLMs (Claude Sonnet 4.6, GPT-4.1, and o4-mini) on two subsets of PARARULE-Plus: a general-purpose sample and a more challenging one targeting a specific failure mode of natural-language reasoning. On the general sample, the formalizer matches or exceeds reasoning LLMs (accuracy 1.00 vs.\ 1.00 / 0.998), with the largest gains over standard models (0.762 for GPT-4.1). On the challenging subset, the formalizer remains near-perfect (1.00 / 0.99) while reasoning LLMs drop to 0.95 / 0.94. These results suggest that delegating inference to Prolog via MCP is a robust and inspectable alternative to extended natural-language reasoning.
Agnieszka Mensfelt, Adarsh Prabhakaran, Adrian Haret +2
Department of Computer Science, Royal Holloway, University of London, UK
We present a framework for evaluating and benchmarking logical reasoning agents when assessment itself must be reproducible, auditable, and robust to execution failures. Building on agentified assessment, we use an assessor agent to issue tasks, enforce execution budgets, parse outputs, and record structured failure types, while the agent under test only needs to expose a standardized agent-to-agent interface. As a case study, we benchmark an auto-formalization agent for first-order logic (FOL) reasoning on a solver-verified and repaired split of FOLIO. The agent translates natural language premises and conclusions into executable Z3Py programs and employs satisfiability modulo theories (SMT) solving to determine logical entailment. On the cleaned FOLIO validation set, the auto-formalization agent achieves 86.70% accuracy under the assessor protocol, outperforming a chain-of-thought baseline (73.89%).