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.

Scenario-based question answering (SQA) has attracted increasing research attention. It typically requires retrieving and integrating knowledge from multiple sources, and applying general knowledge to a specific case described by a scenario. SQA widely exists in the medical, geography, and legal domains—both in practice and in the exams. In this paper, we introduce the GeoSQA dataset. It consists of 1,981 scenarios and 4,110 multiple-choice questions in the geography domain at high school level, where diagrams (e.g., maps, charts) have been manually annotated with natural language descriptions to benefit NLP research. Benchmark results on a variety of state-of-the-art methods for question answering, textual entailment, and reading comprehension demonstrate the unique challenges presented by SQA for future research.