Kimina-Prover-RL

Kimina-Prover-RL est une pipeline open-source d’entraînement pour la démonstration formelle en Lean 4, basée sur une structure pensée en deux étapes (raisonnement puis Lean). Deux modèles open-source (1.7B et 0.6B) atteignent des scores élevés sur MiniF2F. Le projet fournit kimina-lean-server, kimina-client et le dataset Kimina-Prover-Promptset, et se réutilise via un fork Verl.

Source

HuggingFace Blog

Ingested

AUG 14, 2025 · 19:10

Editorial score

4.0 / 5