Introducere: Conceptul și filozofia din spatele Kimina-Prover-RL
Noul pipeline, denumit kimina-prover-rl, reprezintă o versiune simplificată, dar extrem de puternică, a sistemului utilizat pentru a antrena Kimina Prover original. Această versiune păstrează componentele esențiale ale arhitecturii inițiale, oferind în același timp o compatibilitate completă cu framework-ul open-source Verl. Lansarea se materializează printr-un fork al Verl, care conține rețeta completă de antrenare în directorul `recipe/kimina-prover-rl`. Această abordare permite oricărui cercetător sau entuziast să reproducă experimentele echipei sau să adapteze configurația pentru propriile modele și seturi de date, eliminând barierele tehnice care adesea împiedică progresul în acest domeniu de nișă.
Filozofia de bază a kimina-prover-rl este de a învăța modelele de limbaj de mari dimensiuni (LLM) să rezolve obiective de demonstrație formală în Lean 4 printr-o structură de output în două etape distincte. Prima etapă constă într-o urmă de raționament exprimată în limbaj natural, urmată de codul corespunzător în Lean. Această separare a planificării de execuție nu doar că îmbunătățește capacitatea modelului de a generaliza, dar oferă și o explicabilitate crucială – utilizatorii pot înțelege logica din spatele demonstrației înainte de a examina codul formal.
Arhitectura tehnică: Kimina-Client și verificarea la scară largă
Unul dintre cele mai mari provocări în antrenarea modelelor pentru demonstrarea teoremelor este necesitatea verificării simultane a unui număr masiv de candidați. Pentru a gestiona această cerință, echipele Numina și Kimi au dezvoltat „kimina-lean-server”, un server open-source care suportă verificarea paralelă a demonstrațiilor la scară largă folosind Lean 4. Pentru a simplifica integrarea, cercetătorii au pus la dispoziție și „kimina-client”, un pachet Python ușor, disponibil pe PyPI, care oferă o interfață curată pentru interacțiunea cu API-ul serverului. Această infrastructură este vitală pentru faza de „rollout” a algoritmului GRPO (Group Relative Policy Optimization), unde modelul generează multiple output-uri pentru fiecare prompt, iar un sistem de recompensă binar atribuie valoarea 1 doar codurilor Lean verificate cu succes.
Setul de date: Selecția și curarea problemelor complexe
Pentru antrenare, echipa utilizează „Kimina-Prover-Promptset”, un subset curat al setului de date NuminaMath-LEAN. Acest set de date rezultat conține probleme cu valoare ridicată, special selectate pentru dificultatea lor, având ca scop îmbunătățirea modelelor de demonstrare a teoremelor în Lean 4. Este important de menționat că NuminaMath-LEAN-RL este același set de date utilizat pentru a antrena modelele AI-MO/Kimina-Prover-RL-1.7B și AI-MO/Kimina-Prover-RL-0.6B, demonstrând consistența și calitatea datelor selectate.
Mecanismul de recompensă și formatarea structurată
Ideea centrală a pipeline-ului de raționament este structurarea output-ului LLM în două etape obligatorii: un bloc de gândire (`
Corecția erorilor: Învățarea din eșec
Pentru a face antrenamentul mai informativ, cercetătorii au integrat un mecanism inovator de corecție a erorilor. Acesta oferă modelului o șansă de a-și repara propriile demonstrații eșuate. Această abordare încurajează modelul să învețe din semnalele de eșec, deoarece feedback-ul de la Lean este injectat înapoi ca parte a prompt-ului. Astfel, se creează lanțuri de interacțiune multi-turn, unde modelul este recompensat pentru depanarea cu succes a propriului output. Pentru a gestiona complexitatea, este permis doar un singur turn de corecție a erorilor, iar mesajele de eroare sunt limitate la un număr stabilit de token-uri.
Optimizare și combaterea bias-ului de lungime: DrGRPO
O contribuție teoretică importantă a acestui proiect este utilizarea DrGRPO (Distance-scaled Group Relative Policy Optimization). Studiile recente, precum „Understanding R1-Zero-Like Training: A Critical Perspective”, au evidențiat existența unui bias de optimizare în GRPO standard, care duce la răspunsuri artificial mai lungi, în special pentru output-urile incorecte. Echipa Kimina a observat acest comportament în experimentele lor și a implementat DrGRPO, care normalizează pierderile la nivel de token printr-o constantă globală, eliminând astfel bias-ul de lungime și asigurând o optimizare mai echilibrată.
Rezultatele experimentale: Performanță și scalare
După 48 de ore de antrenament pe 8 GPU-uri H100, rezultatele sunt remarcabile. La pasul 85 de antrenament, pipeline-ul a îmbunătățit acuratețea modelului cu 4 puncte, atingând 70% pentru metrica best@8 și 74% după turnul de corecție a erorilor. În paralel, numărul de erori de formatare a scăzut constant, confirmând că modelul învață să producă output-uri valide structural. Așa cum era de așteptat în regimul de antrenament DeepSeek-R1, lungimea medie a token-ilor în output-uri a crescut, semnalând capacitatea modelului de a efectua raționamente mai lungi și mai structurate.
Evaluarea finală folosind metrica pass@32 pe setul de date MiniF2F arată îmbunătățiri semnificative. Modelul AI-MO/Kimina-Prover-RL-1.7B a atins 76,23% (fără corecție) și 77,87% (cu corecție), comparativ cu modelul de bază care stagna la 72,95%. Similar, modelul de 0,6B parametri a înregistrat o îmbunătățire de peste 2%, atingând 71,30%.
Concluzie
Prin lansarea Kimina-Prover-RL, echipa oferă comunității un instrument robust și accesibil pentru antrenarea demonstratorilor de teoreme în Lean 4. Combinând raționamentul structurat, recompensele de format și corecția erorilor, acest pipeline stabilește un nou standard pentru modelele open-source din gama 0,6B–1,7B parametri. Această lansare nu doar că validează eficiența învățării prin întărire în raționamentul formal, dar deschide și calea pentru inovații viitoare în demonstrarea automată a teoremelor, o componentă critică pentru verificarea corectitudinii software-ului și a demonstrațiilor matematice complexe.
