@inproceedings{li-etal-2026-learning-explore,
title = "Learning to Explore the Crux in Formal Theorem Proving",
author = "Li, Linhan and
Cui, Wenyao and
Zhang, Gong-Duo and
Gu, Lihong and
Zhou, Lin and
Shang, Jianyun and
Zhang, Huaping",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.emnlp-main.1932/",
pages = "43958--43979",
ISBN = "979-8-89176-459-0",
abstract = "Recent advancements in the application of Large Language Models (LLMs) to formal theorem proving in Lean have unveiled new prospects in complex logical reasoning scenarios. Acknowledging that the difficulty across reasoning steps in a formal theorem proof is not uniform, prior proof search algorithms have not systematically investigated which proof steps are more crucial to explore. This paper introduces $\textbf{E}$ntropy-Based $\textbf{B}$est-$\textbf{F}$irst $\textbf{S}$earch (EBFS), an entropy-inspired heuristic tree search algorithm that enhances the efficiency of proof generation models to explore proof trees, thereby increasing the probability of finding the correct proof. We also introduce a reinforcement fine-tuning approach specifically for proof tree search. Using EBFS during the generation stage further boosts the model{'}s performance in proof generation. Evaluations demonstrate that our fine-tuned EBFS model achieves consistent improvements over the baseline models. Under the same sample budget, it outperforms whole proof generation by 3.2{\%} on the ProofNet testset, with further gains of 1.9{\%} on MiniF2F and 1.5{\%} on ProverBench."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="li-etal-2026-learning-explore">
<titleInfo>
<title>Learning to Explore the Crux in Formal Theorem Proving</title>
</titleInfo>
<name type="personal">
<namePart type="given">Linhan</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Wenyao</namePart>
<namePart type="family">Cui</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Gong-Duo</namePart>
<namePart type="family">Zhang</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Lihong</namePart>
<namePart type="family">Gu</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Lin</namePart>
<namePart type="family">Zhou</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jianyun</namePart>
<namePart type="family">Shang</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Huaping</namePart>
<namePart type="family">Zhang</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hung-Yi</namePart>
<namePart type="family">Lee</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sunipa</namePart>
<namePart type="family">Dev</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jessy</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Desmond</namePart>
<namePart type="family">Elliott</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-459-0</identifier>
</relatedItem>
<abstract>Recent advancements in the application of Large Language Models (LLMs) to formal theorem proving in Lean have unveiled new prospects in complex logical reasoning scenarios. Acknowledging that the difficulty across reasoning steps in a formal theorem proof is not uniform, prior proof search algorithms have not systematically investigated which proof steps are more crucial to explore. This paper introduces Entropy-Based Best-First Search (EBFS), an entropy-inspired heuristic tree search algorithm that enhances the efficiency of proof generation models to explore proof trees, thereby increasing the probability of finding the correct proof. We also introduce a reinforcement fine-tuning approach specifically for proof tree search. Using EBFS during the generation stage further boosts the model’s performance in proof generation. Evaluations demonstrate that our fine-tuned EBFS model achieves consistent improvements over the baseline models. Under the same sample budget, it outperforms whole proof generation by 3.2% on the ProofNet testset, with further gains of 1.9% on MiniF2F and 1.5% on ProverBench.</abstract>
<identifier type="citekey">li-etal-2026-learning-explore</identifier>
<location>
<url>https://aclanthology.org/2026.emnlp-main.1932/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>43958</start>
<end>43979</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T Learning to Explore the Crux in Formal Theorem Proving
%A Li, Linhan
%A Cui, Wenyao
%A Zhang, Gong-Duo
%A Gu, Lihong
%A Zhou, Lin
%A Shang, Jianyun
%A Zhang, Huaping
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-459-0
%F li-etal-2026-learning-explore
%X Recent advancements in the application of Large Language Models (LLMs) to formal theorem proving in Lean have unveiled new prospects in complex logical reasoning scenarios. Acknowledging that the difficulty across reasoning steps in a formal theorem proof is not uniform, prior proof search algorithms have not systematically investigated which proof steps are more crucial to explore. This paper introduces Entropy-Based Best-First Search (EBFS), an entropy-inspired heuristic tree search algorithm that enhances the efficiency of proof generation models to explore proof trees, thereby increasing the probability of finding the correct proof. We also introduce a reinforcement fine-tuning approach specifically for proof tree search. Using EBFS during the generation stage further boosts the model’s performance in proof generation. Evaluations demonstrate that our fine-tuned EBFS model achieves consistent improvements over the baseline models. Under the same sample budget, it outperforms whole proof generation by 3.2% on the ProofNet testset, with further gains of 1.9% on MiniF2F and 1.5% on ProverBench.
%U https://aclanthology.org/2026.emnlp-main.1932/
%P 43958-43979
Markdown (Informal)
[Learning to Explore the Crux in Formal Theorem Proving](https://aclanthology.org/2026.emnlp-main.1932/) (Li et al., EMNLP 2026)
ACL
- Linhan Li, Wenyao Cui, Gong-Duo Zhang, Lihong Gu, Lin Zhou, Jianyun Shang, and Huaping Zhang. 2026. Learning to Explore the Crux in Formal Theorem Proving. In Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing, pages 43958–43979, Budapest, Hungary. Association for Computational Linguistics.