Hugging Face开源Kimina-Prover-RL训练管线及Lean 4定理证明模型

Hugging Face开源了Kimina-Prover-RL，一个基于Verl框架的Lean 4形式化定理证明训练管线，并发布了1.7B和0.6B两个模型。该管线采用类DeepSeek-R1的结构化推理范式，结合格式奖励和错误纠正机制，在MiniF2F基准上刷新了开源模型在对应参数规模下的SOTA成绩。