title: Leanabell-Prover: Posttraining Scaling in Formal Reasoning
summary: Recent advances in automated theorem proving (ATP) through LLMs have
  highlighted the potential of formal reasoning with Lean 4 codes. However, ATP
  has not yet be revolutionized by the recent posttraining scaling as
  demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the
  entire posttraining of ATP, aiming to align it with breakthroughs in reasoning
  models in natural languages.To begin, we continual train current ATP models
  with a hybrid dataset, which consists of numerous statement-proof pairs, and
  additional data aimed at incorporating cognitive behaviors that emulate human
  reasoning and hypothesis refinement. Next, we explore reinforcement learning
  with the use of outcome reward returned by Lean 4 compiler. Through our
  designed continual training and reinforcement learning processes, we have
  successfully improved existing formal provers, including both
  DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance
  in the field of whole-proof generation. For example, we achieve a 59.8% pass
  rate (pass@32) on MiniF2F. This is an on-going project and we will
  progressively update our findings, release our data and training details.
paper_authors._id: 67f664cc902987500a49b197
paper_authors.name: Jingyuan Zhang
paper_authors._id: 67f664cc902987500a49b198
paper_authors.name: Qi Wang
paper_authors._id: 67f664cc902987500a49b199
paper_authors.name: Xingguang Ji
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2025-04-09T16:50:19.951Z
paper_authors._id: 66a8b5ea275e4553e3e161f8
paper_authors.avatarUrl: /avatars/422e25450133c1c04749aab9ae39f9b4.svg
paper_authors.fullname: jxg
paper_authors.type: user
paper_authors.user: jixingguang
paper_authors._id: 67f664cc902987500a49b19a
paper_authors.name: Yahui Liu
paper_authors._id: 67f664cc902987500a49b19b
paper_authors.name: Yang Yue
paper_authors._id: 67f664cc902987500a49b19c
paper_authors.name: Fuzheng Zhang
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2025-04-09T16:50:50.399Z
paper_authors._id: 67c5945da1661d5fa6f29adb
paper_authors.avatarUrl: /avatars/62561f3875c0c251cae949acc38d72dc.svg
paper_authors.fullname: Fuzheng Zhang
paper_authors.type: user
paper_authors.user: Edrex
paper_authors._id: 67f664cc902987500a49b19d
paper_authors.name: Di Zhang
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2025-04-09T16:50:56.751Z
paper_authors._id: 644c8324f02250233d0d67d9
paper_authors.avatarUrl: /avatars/feb39d281457c1750f3eada3c060a23e.svg
paper_authors.fullname: Di Zhang
paper_authors.type: user
paper_authors.user: dizhang
paper_authors._id: 67f664cc902987500a49b19e
paper_authors.name: Guorui Zhou
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2025-04-09T16:51:02.310Z
paper_authors._id: 67c6c570cf87e2d2ebfc81aa
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/67c6c570cf87e2d2ebfc81aa/7qAstZtIT86Uwrz3u_anv.jpeg
paper_authors.fullname: Guorui Zhou
paper_authors.type: user
paper_authors.user: GuoruiZhou
paper_authors._id: 67f664cc902987500a49b19f
paper_authors.name: Kun Gai
paper_title: Leanabell-Prover: Posttraining Scaling in Formal Reasoning
paper_summary: Recent advances in automated theorem proving (ATP) through LLMs have
  highlighted the potential of formal reasoning with Lean 4 codes. However, ATP
  has not yet be revolutionized by the recent posttraining scaling as
  demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the
  entire posttraining of ATP, aiming to align it with breakthroughs in reasoning
  models in natural languages.To begin, we continual train current ATP models
  with a hybrid dataset, which consists of numerous statement-proof pairs, and
  additional data aimed at incorporating cognitive behaviors that emulate human
  reasoning and hypothesis refinement. Next, we explore reinforcement learning
  with the use of outcome reward returned by Lean 4 compiler. Through our
  designed continual training and reinforcement learning processes, we have
  successfully improved existing formal provers, including both
  DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance
  in the field of whole-proof generation. For example, we achieve a 59.8% pass
  rate (pass@32) on MiniF2F. This is an on-going project and we will
  progressively update our findings, release our data and training details.
paper_ai_summary: Continual training and reinforcement learning of ATP models using Lean 4 improve formal provers and achieve state-of-the-art performance in whole-proof generation.
paper_ai_keywords: continual training reinforcement learning Lean 4 provers whole-proof generation MiniF2F pass rate