მოხარულნი ვართ წარმოგიდგინოთ kimina-prover-rl, ღია კოდის სასწავლო კონვეიერი Lean 4-ში ფორმალური თეორემების დამტკიცებისთვის, რომელიც DeepSeek-R1-ის მიერ შთაგონებულ სტრუქტურირებულ მსჯელობა-შემდეგ-გენერაციის პარადიგმას ეფუძნება. ეს სასწავლო კონვეიერი წარმოადგენს იმ სისტემის გამარტივებულ ვერსიას, რომელიც Kimina Prover-ის მოსამზადებლად გამოვიყენეთ. ის ინარჩუნებს სისტემის ძირითად კომპონენტებს და გთავაზობთ სრულ თავსებადობას ღია კოდის Verl ფრეიმვორკთან. პროექტი გამოქვეყნებულია Verl-ის ფორკის სახით, რომელიც სრულ სასწავლო რეცეპტს შეიცავს `recipe/kimina-prover-rl` განყოფილებაში, რაც ნებისმიერ მსურველს საშუალებას აძლევს გაიმეოროს ჩვენი ექსპერიმენტები ან მოარგოს პარამეტრები საკუთარ მოდელებსა და მონაცემთა ნაკრებებს. კონვეიერის დაყენებისა და გაშვებისთვის საჭირო ყველა ინფორმაცია შეგიძლიათ იხილოთ რეცეპტის README ფაილში. ამ სასწავლო კონვეიერის შედეგად, ჩვენ ორ მოდელს ვუშვებთ: kimina-prover-rl არის სასწავლო კონვეიერი, რომელიც მიზნად ისახავს დიდი ენობრივი მოდელებისთვის (LLMs) Lean 4-ში ფორმალური დამტკიცების მიზნების გადაჭრის სწავლებას, ორეტაპიანი გამომავალი სტრუქტურის გამოყენებით: ბუნებრივი ენის მსჯელობის კვალი, რასაც მოსდევს შესაბამისი Lean კოდი. DeepSeek-R1-ის მიერ შთაგონებული ეს პარადიგმა მოდელს საშუალებას აძლევს დაგეგმვა და შესრულება ერთმანეთისგან გამიჯნოს, რაც ხელს უწყობს ახსნადობას, შეცდომების აღდგენასა და ძლიერ განზოგადებას. ამ მსჯელობის ფრეიმვორკის ფარგლებში მოდელების მოსამზადებლად, ჩვენ ვიყენებთ GRPO-ს – გაძლიერებითი სწავლის მიდგომას, რომელიც სპეციალურად LLM-ებისთვისაა შექმნილი. Kimina-prover-ის სასწავლო კონვეიერის ეს ღია კოდის ვერსია დანერგილია RL ბიბლიოთეკა Verl-ის გამოყენებით. GRPO-ის გაშლის (rollout) ფაზის დროს, მოდელი თითოეული მოთხოვნისთვის (prompt) N გამოსავალს აგენერირებს. 1 ქულის ჯილდო ენიჭება ნებისმიერ გამოსავალს, რომლის Lean კოდიც წარმატებით დამოწმებულია Lean-ის მიერ ჩვენი kimina-lean-server-ის გამოყენებით. ამ ფრეიმვორკს ორი ძირითადი ფუნქცია დაემატა: სწავლის პროცესში, Lean 4-ის მტკიცებულების კანდიდატების დიდი რაოდენობა ერთდროულად უნდა დამოწმდეს. ამის ეფექტურად სამართავად, ჩვენ გვჭირდება მაღალეფექტური ვალიდაციის სისტემა. ამ საჭიროების დასაკმაყოფილებლად, Numina-მ და Kimi-მ შეიმუშავეს ღია კოდის სერვერი სახელწოდებით kimina-lean-server, რომელიც მხარს უჭერს პარალელურ მტკიცებულებათა შემოწმებას დიდი მასშტაბით Lean 4-ის გამოყენებით. ინტეგრაციის გასამარტივებლად, ჩვენ ასევე გთავაზობთ kimina-client-ს, მსუბუქ Python პაკეტს (ხელმისაწვდომია PyPI-ზე), რომელიც სერვერის API-სთან ურთიერთობისთვის მარტივ ინტერფეისს გვთავაზობს. ჩვენ ვავარჯიშებთ Kimina-Prover-Promptset-ის გამოყენებით, რომელიც წარმოადგენს NuminaMath-LEAN მონაცემთა ნაკრების შერჩეულ ქვენაკრებს. ამ სასწავლო კონფიგურაციისთვის, ჩვენ მონაცემთა ნაკრებს შემდეგნაირად ვფილტრავთ და ვამუშავებთ წინასწარ: მიღებული მონაცემთა ნაკრები შეიცავს რთულ, მაღალი ღირებულების პრობლემებს Lean 4-ის თეორემების დამამტკიცებელი მოდელების გასაუმჯობესებლად. NuminaMath-LEAN-RL ასევე არის მონაცემთა ნაკრები, რომელიც გამოიყენება AI-MO/Kimina-Prover-RL-1.7B და AI-MO/Kimina-Prover-RL-0.6B მოდელების მოსამზადებლად. შეყვანის მაგალითის ფორმატი: ჩვენი მსჯელობითი სასწავლო კონვეიერის მთავარი იდეაა LLM-ის გამომავალი ორ ეტაპად დაყოფა: ერთი აზროვნების ბლოკი, რასაც მოჰყვება ერთი lean4 ბლოკი. თითოეული გაშლა (rollout) მოწმდება იმის უზრუნველსაყოფად, რომ ეს ფორმატი დაცულია. თუ გამომავალი არასწორადაა ფორმატირებული – მაგალითად, აკლია ბლოკი ან არასწორადაა განთავსებული კოდი – მოდელი იღებს ნულოვან ჯილდოს, მიუხედავად იმისა, არის თუ არა მტკიცებულება რეალურად ვალიდური. ეს უზრუნველყოფს თანმიმდევრულობას და ასწავლის მოდელს გამომავლის საიმედოდ სტრუქტურირებას. kimina-prover-ში, ეს შემოწმებები სცდება უბრალოდ და lean4 ბლოკების არსებობის შემოწმებას: მხოლოდ ის გენერაციები, რომლებიც ყველა ამ შემოწმებას გაივლიან, მიიჩნევა სწორად ფორმატირებულად და შეუძლია მიიღოს ჯილდო. ეს სტრუქტურირებული ფილტრაცია აუმჯობესებს სწავლის სტაბილურობას და ხელს უწყობს მკაფიო მსჯელობას. სწავლის უფრო ინფორმატიული გასახდომად, ჩვენ დავამატეთ შეცდომების გამოსწორების მექანიზმი, რომელიც მოდელს აძლევს შანსს გამოასწოროს საკუთარი წარუმატებელი მტკიცებულებები. როდესაც გაშლა (rollout) მარცხდება (მაგალითად, Lean შეცდომის ან არასწორი მტკიცებულების გამო), სისტემა მოდელს აწვდის უკუკავშირს შეცდომის შესახებ. ეს მოდელს აძლევს სტიმულს, ისწავლოს წარუმატებლობის სიგნალებიდან, რადგან სწავლის პროცესში მიწოდებულია უკუკავშირი Lean-ისგან. ის ასევე შესაძლებელს ხდის მრავალმხრივი ურთიერთქმედების ჯაჭვებს, სადაც Lean-ის უკუკავშირი ჩართულია მოთხოვნის ნაწილად და მოდელი ჯილდოვდება საკუთარი გამომავლის წარმატებით გამართვისთვის. რადგან მრავალმხრივი პასუხები შეიძლება გრძელი იყოს, ჩვენ მხოლოდ ერთ შეცდომის გამოსწორების რაუნდს ვუშვებთ და შეცდომის შეტყობინებას სიმბოლოების დადგენილ რაოდენობამდე ვზღუდავთ. ნაშრომი „Understanding R1-Zero-Like Training: A Critical Perspective“ ამტკიცებს, რომ GRPO-ში არსებობს ოპტიმიზაციის მიკერძოება, რაც ხელოვნურად ახანგრძლივებს პასუხებს, განსაკუთრებით არასწორი გამომავლების შემთხვევაში. ჩვენც შევამჩნიეთ ეს ქცევა ჩვენი ექსპერიმენტების დროს და ოპტიმიზაციისთვის DrGRPO გამოვიყენეთ. DrGRPO აგროვებს სიმბოლოების (token) დონის დანაკარგებს გლობალური მუდმივით ნორმალიზების გზით, რათა აღმოფხვრას სიგრძის მიკერძოება. საცავში მოწოდებული კონფიგურაციის ფაილი განკუთვნილია 8 GPU-სთვის. მოდელი, რომელსაც ვაწვრთნით, არის AI-MO/Kimina-Prover-Distill-1.7B. ეს მოდელი წარმოადგენს Qwen/Qwen3-1.7B-ის დახვეწილ ვერსიას (finetuned), ცივი სტარტის მონაცემებით, რომლებიც გენერირებულია ჩვენი AI-MO/Kimina-Prover-72B მოდელისგან. ყოველ ნაბიჯზე, სასწავლო მონაცემთა ნაკრებიდან ამოღებულია 256 ნიმუში. ყოველი ორი ნიმუშიდან ერთი არის შეცდომის გამოსწორების ნიმუში. ჩვენ ვაგენერირებთ 8 გაშლას (rollout) თითო ნიმუშზე, ანუ 2048 გენერაციას. შეგიძლიათ გაზარდოთ 16 ან 32 გაშლამდე, თუ იყენებთ ერთზე მეტ კვანძს. მოდელს ვაფასებთ ყოველ 5 სასწავლო ნაბიჯზე, verl-ის best@8 მეტრის გამოყენებით, რათა მივიღოთ სწრაფი ვალიდაციის ნაბიჯები. შეგიძლიათ გაზარდოთ best@16 ან 32-მდე, თუ ერთზე მეტ კვანძს იყენებთ.