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

Zhiyu Ni; Zheng Liang; Liangcheng Song; Chenrui Cao; Xian Zhang; Alberto Sangiovanni-Vincentelli; Pierluigi Nuzzo

cs.AIMar 18, 2026

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

Authors: Zhiyu Ni, Zheng Liang, Liangcheng Song, Chenrui Cao, Xian Zhang, Alberto Sangiovanni-Vincentelli, Pierluigi Nuzzo

Organizations: University of California, Berkeley · Microsoft

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 & tables

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

Panel of Figure 3 — Figure 3: A correct Z3Py program corresponds to an input question in AR-LSAT

Panel of Figure 4 — Figure 4: Two typical types of ill-defined logical programs which can be detected during inference

Paradigm	Method	Fallback	LLM	End-to-end Accuracy (%)
Paradigm	Method	Policy	LLM	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 (

\mathbf{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	$\mathbf{Acc}$ (%)	$\mathbf{Exec}$ $\mathbf{Rate}$ (%)	$\mathbf{Acc}$ (%) $\mathbf{@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 (

\mathrm{cover}@k

) as a function of the number of sampled AF paths

k

across four benchmarks.

	$\mathbf{Acc}_{\mathrm{AF}}$ (%)
	AF w/o draft	AF w/ draft
AR-LSAT	36.35 $\pm$ 1.22	41.78 $\pm$ 2.46
ProofWriter	97.69 $\pm$ 0.18	98.33 $\pm$ 0.22
PrOntoQA	94.92 $\pm$ 0.84	99.56 $\pm$ 0.18
LogicalDeduction	98.60 $\pm$ 0.58	98.23 $\pm$ 0.32

Table 3: Accuracy with a naive AF path w/ and w/o drafted plans (on GPT-4, w/o pruning).

Panel of Figure 6 — Figure 6: Diagnostic metrics on ProofWriter across different numbers of paths ( $k$ ).

Figure 7:

\mathbf{Acc}_{\mathrm{AF}}

on AR-LSAT w/o vs. w/ pruning across different numbers of paths (

k

). Without pruning, the

\mathbf{Acc}_{\mathrm{AF}}

plateaus around

45\%

quickly, while pruning enables further accuracy boost to around

78\%

	$\mathbf{Acc}_{\mathrm{AF}}$ (%)
	w/o Pruning	w/ Pruning
AR-LSAT	45.13 $\pm$ 0.34	78.43 $\pm$ 0.55
ProofWriter	98.33 $\pm$ 0.00	98.33 $\pm$ 0.00
PrOntoQA	99.34 $\pm$ 0.10	99.32 $\pm$ 0.10
LogicalDeduction	99.33 $\pm$ 0.00	99.50 $\pm$ 0.18

Table 4: The

\mathbf{Acc}_{\mathrm{AF}}

(%) of D&P w/o vs. w/ pruning on four benchmarks. There are twenty paths (

k=20

), and every path uses drafted plans.

Panel of Figure 8 — 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

Panel of Figure 9 — Figure 9: AF-only accuracy versus $k$ for D&P without pruning and D&P with pruning on AR-LSAT.

Panel of Figure 10 — 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

$T_{\text{DRAFT}}$	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

$T_{\text{DRAFT}}$	Acc@k20 (%)	PathAcc (%)	HitRate@k20 (%)	$H_{\mathrm{avg}}^{\mathrm{norm}}$
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).

Autoformalization

Autoformalization converts natural-language mathematics, proofs, and specifications into machine-checkable formal languages.

See all 115 papers

FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
Aug 11, 2026Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh +7CoT Faithfulness LLM Sycophancy
Nanyang Technological University, Singapore · University of Oxford, United Kingdom · The University of Edinburgh, United Kingdom
PrologMCP: A Standardized Prolog Tool Interface for LLM Agents
Jun 12, 2026Agnieszka Mensfelt, Adarsh Prabhakaran, Adrian Haret +2Logic Programming Symbolic Reasoning
Department of Computer Science, Royal Holloway, University of London, UK
Agentified Assessment of Logical Reasoning Agents
Mar 3, 2026Zhiyu Ni, Yifeng Xiao, Zheng LiangLLM Agent Evaluation AI Agent Benchmarks
University of California, Berkeley

Aug 11, 2026J/K move · Enter open · S save

FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation

Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh, Shuqi Liu+6

Nanyang Technological University, Singapore · University of Oxford, United Kingdom · The University of Edinburgh, United Kingdom

CoT Faithfulness LLM Sycophancy Autoformalization

Open paper AskPDF arXiv

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.

Abstract

Autoformalization

Explore similar work

FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation

PrologMCP: A Standardized Prolog Tool Interface for LLM Agents

Agentified Assessment of Logical Reasoning Agents