Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Formal Theorem Generation via MCTS with LLM-Guided Process Optimization

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Lei Wang,
  • Zhengfeng Yang

摘要

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.