Formal Theorem Generation via MCTS with LLM-Guided Process Optimization

While large language models (LLMs) have shown great potential in formal theorem proving tasks, their performance is limited by the scarcity of formal theorem data. To address this issue, we propose a formal theorem generation method aimed at providing high-quality fine-tuning training data in Lean4 for LLMs. We propose a Training-Free Policy-Value framework for Monte Carlo Tree Search (MCTS-TFPV). We introduce LLM-generated policy probabilities combined with dynamic temperature annealing to optimize the search process, along with a rule-based value function to dynamically evaluate the quality of generated theorems. Our method replaces traditional policy and value networks with a rule-based design, optimizing the theorem generation process to significantly reduce computational costs while enhancing the quality of generated theorems. Experiments are conducted on Llama3-8B and Qwen2.5-7B, with comprehensive comparisons against traditional methods. The results show that our method significantly improves performance in formal theorem generation tasks, offering an efficient and scalable solution for LLMs in formal mathematical tasks.