მოხარულნი ვართ გამოვაცხადოთ Kimina-Prover-72B-ის გამოშვება, ჩვენი უახლესი თეორემის დამტკიცების მოდელი, რომელიც გაწვრთნილია Kimi k1.5[1] განმტკიცებითი სწავლის (RL) სისტემით და დაფუძნებულია Qwen2.5-72B-ზე [2]. მასთან ერთად, ჩვენ ასევე ვუშვებთ ორ დისტილირებულ ვარიანტს: Kimina-Prover-Distill-8B და 1.7B (შესაბამისად Qwen3-8B-სა და Qwen3-1.7B-ზე [3] დაფუძნებულს). ჩვენი ძირითადი ინოვაციები მოიცავს: ტესტირების დროს განმტკიცებითი სწავლის ძიება (Test-Time Reinforcement Learning Search): გაწვრთნადი აგენტური დამტკიცების ფრეიმვორკი, რომელიც მოდელს საშუალებას აძლევს რეკურსიულად აღმოაჩინოს, დააკავშიროს და გამოიყენოს მრავალი ლემა კომპლექსური მტკიცებულებების ასაგებად, ახალი ლემების მხარდაჭერითი შაბლონის საფუძველზე. შეცდომების გამოსწორების შესაძლებლობა: Kimina-Prover-ს შეუძლია წაიკითხოს და განმარტოს Lean-ის შეცდომის შეტყობინებები და შესთავაზოს მიზანმიმართული გამოსწორებები, რაც მნიშვნელოვნად მაღალ ნიმუშის ეფექტურობას აჩვენებს მტკიცებულებების ნულიდან ხელახლა გენერირებასთან შედარებით. ეს მიღწევები Kimina-Prover-ს აძლევს საშუალებას, გადაჭრას რთული მათემატიკური ამოცანები და გადააჭარბოს წინა მეთოდებს. როგორც ნაჩვენებია სურათ 1-ზე, ფართოდ გამოყენებულ miniF2F ბენჩმარკზე, Kimina-Prover აღწევს უახლეს 92.2%-იან წარმატებას. ჩვენ ფოკუსირებული ვართ ავტომატურ თეორემის დამტკიცებაზე (ATP) Lean 4 ენაზე, მიზნად ვისახავთ ფორმალური მათემატიკური მტკიცებულებების კონსტრუქციის ავტომატიზაციას. ნეირონული თეორემის დამტკიცების ბოლო მიღწევებმა მნიშვნელოვნად გააუმჯობესა ხელოვნური ინტელექტის სისტემების უნარი, დაეხმარონ ან მოახდინონ ამ პროცესის ავტომატიზაცია. აღსანიშნავი პროგრესი მოიცავს Google DeepMind-ის AlphaProof[4]-ს, რომელმაც ძლიერი შესრულება აჩვენა საერთაშორისო მათემატიკური ოლიმპიადის დონის ამოცანებზე. ღია წყაროს სისტემებმა, როგორიცაა DeepSeek-Prover-V2[5], რომელიც მოიცავს განმტკიცებით სწავლებას, ასევე მიაღწიეს უახლეს შედეგებს. გარდა ამისა, ნეირო-სიმბოლურმა აგენტურმა მიდგომებმა, როგორიცაა DSP+[6], აჩვენეს, რომ კონკურენტული შესრულება შესაძლებელია ფართომასშტაბიანი სწავლების გარეშე, მოდულურ ფრეიმვორკში მზა მოდელების გამოყენებით. ჩვენმა ადრინდელმა ნაშრომმა, Kimina-Prover Preview[7], წარმოადგინა დიდი ენობრივი მოდელი Lean-ში ფორმალური თეორემის დამტკიცებისთვის, დაამყარა ახალი შესრულების საწყისი დონე miniF2F ბენჩმარკზე. ფართომასშტაბიანი განმტკიცებითი სწავლის სისტემით გაწვრთნილი მოდელი იყენებდა მსჯელობაზე ორიენტირებული ძიების პარადიგმას და აჩვენა, რომ უფრო დიდ მოდელებს შეუძლიათ უფრო ძლიერი ფორმალური მსჯელობის შემსრულებლების როლი შეასრულონ. მისი სტრუქტურირებული მსჯელობის შაბლონი უზრუნველყოფდა მტკიცებულებების ეფექტურ ძიებას და ადამიანის მსგავსი პრობლემის გადაჭრის სტრატეგიებს. ამ საწყისი წარმატების შემდეგ, ჩვენ გავაგრძელეთ მოდელის გაუმჯობესება განმტკიცებითი სწავლის შემდგომი იტერაციების მეშვეობით. თუმცა, ერთსაფეხურიანი მსჯელობა კვლავ არასაკმარისია რთული ამოცანების გადასაჭრელად, რომლებიც გრძელ, მრავალსაფეხურიან მტკიცებულებებს მოითხოვს. ამ შეზღუდვის აღმოსაფხვრელად, ჩვენ წარმოგიდგენთ ტესტირების დროს განმტკიცებითი სწავლის (TTRL) საძიებო ფრეიმვორკს, რომელიც მოდელს საშუალებას აძლევს ავტონომიურად აღმოაჩინოს, დააკავშიროს და ხელახლა გამოიყენოს მრავალი შუალედური ლემა. ეს ფრეიმვორკი მხარს უჭერს უფრო ღრმა, ხანგრძლივ მსჯელობას რთული პრობლემების ხელახლა გამოსაყენებელ ქვეკომპონენტებად დაშლით. TTRL ძიების ერთ-ერთი მთავარი კომპონენტია ლემების მხარდაჭერითი შაბლონი, რომელიც მოდელს საშუალებას აძლევს ამოიცნოს და გამოიყენოს შუალედური ლემები თავისი მტკიცებულებების კონსტრუქციის პროცესის ნაწილად. შუალედური შედეგების ეს სტრუქტურირებული ხელახალი გამოყენება მნიშვნელოვნად აფართოებს მოდელის პრობლემის გადაჭრის შესაძლებლობას ერთსაფეხურიანი გენერაციის მიღმა. მდგრადობის შემდგომი გასაუმჯობესებლად, ჩვენ ასევე ვაერთიანებთ შეცდომების გამოსწორების მექანიზმს, რომელიც განმარტავს Lean-ის შეცდომის შეტყობინებებს და გვთავაზობს მიზანმიმართულ კორექტირებებს. ეს მოდელს საშუალებას აძლევს დახვეწოს თავისი შედეგები განმეორებითი უკუკავშირის მეშვეობით, აუმჯობესებს მტკიცებულებების სანდოობას და ნიმუშის საერთო ეფექტურობას. ვინაიდან შემოთავაზებული ტექნიკის კომბინაცია იწვევს მნიშვნელოვან გაუმჯობესებებს ფორმალური თეორემის დამტკიცების შესრულებაში. miniF2F ბენჩმარკზე, Kimina-Prover აღწევს 84.0%-იან წარმატებას pass@32-ით და 86.4%-ს შეცდომის გამოსწორების ერთი რაუნდის დამატებით. pass@1024-ით, წარმატების მაჩვენებელი აღწევს 87.7%-ს. სრულყოფილი ტესტირების დროს განმტკიცებითი სწავლის (TTRL) საძიებო ფრეიმვორკის გამოყენება იძლევა საბოლოო წარმატების მაჩვენებელს 92.2%-ს, სავარაუდო ზედა ზღვრით დაახლოებით 42,000. თუმცა, წარმატების ეს ბიუჯეტი მნიშვნელოვნად შეიძლება ოპტიმიზირდეს მომავალ ვერსიებში, რადგან ამჟამინდელი შერჩევის დიდი ნაწილი იხარჯება უსარგებლო ან ზედმეტი ლემების დამტკიცებაზე. აღსანიშნავია, რომ ეს შედეგები მიუთითებს დამამტკიცებლის მასშტაბირების ქცევის ცვლილებაზე. მაშინ როდესაც ადრინდელი ვერსიები აჩვენებდნენ დაახლოებით ხაზოვან გაუმჯობესებას ლოგარითმულ მასშტაბში შერჩევის ბიუჯეტის ზრდით, მიმდინარე სისტემა აჩვენებს შემცირებულ ეფექტურობას pass@1024-ის მიღმა. ეს იმაზე მეტყველებს, რომ შემდგომი მიღწევები ნაკლებად არის დამოკიდებული გაზრდილ შერჩევაზე და უფრო მეტად მოითხოვს დახვეწილ საძიებო სტრატეგიებს, როგორიცაა TTRL-ის მიერ შემოთავაზებული. ლემების მხარდაჭერითი შაბლონი შექმნილია იმისთვის, რომ მოდელს მიანიჭოს შემავალ მონაცემებში მოწოდებული სასარგებლო ლემების ამოცნობისა და გამოყენების უნარი. ამ შესაძლებლობის მხარდასაჭერად, განმტკიცებითი სწავლის (RL) ვარჯიშის დროს, პრობლემის კონტექსტს წინ ემატება ერთი-სამი ფორმალური ლემის შემთხვევითი ქვესიმრავლე, რაც დამამტკიცებელს აცნობს პოტენციურად სასარგებლო შუალედურ შედეგებს, რომლებსაც შეუძლიათ ხელი შეუწყონ საბოლოო მტკიცებულების კონსტრუქციას. ეს ლემები მზადდება ორსაფეხურიანი სისტემით: (1) გე