Numina-სა და Kimi-ის გუნდი: Kimina-Prover-72B-ის გამოშვება
Numina-მ და Kimi-მ წარმოადგინეს Kimina-Prover-72B, უახლესი ხელოვნური ინტელექტის მოდელი თეორემების დამტკიცებისთვის, რომელიც გაწვრთნილია Kimi k1.5 RL სისტემით და დაფუძნებულია Qwen2.5-72B-ზე. მოდელის ძირითადი ინოვაციებია ტესტირების დროს განმტკიცებითი სწავლის ძიება (TTRL) რთული, მრავალსაფეხურიანი მტკიცებულებებისთვის ლემების გამოყენებით და შეცდომების გამოსწორების შესაძლებლობა, რაც მნიშვნელოვნად ზრდის ეფექტურობას. Kimina-Prover-მა მიაღწია 92.2%-იან უპრეცედენტო წარმატებას miniF2F ბენჩმარკზე, რამაც მას
წარმოგიდგენთ kimina-prover-rl-ს: ღია კოდის სასწავლო კონვეიერს Lean 4-ში ფორმალური თეორემების დამტკიცებისთვის
kimina-prover-rl არის ღია კოდის სასწავლო კონვეიერი Lean 4-ში ფორმალური თეორემების დასამტკიცებლად, რომელიც DeepSeek-R1-ის მიერ შთაგონებულ სტრუქტურირებულ მსჯელობა-შემდეგ-გენერაციის პარადიგმას ეფუძნება. ის წარმოადგენს Kimina Prover სისტემის გამარტივებულ ვერსიას, თუმცა ინარჩუნებს ძირითად კომპონენტებს და სრულად თავსებადია Verl ფრეიმვორკთან. მისი მიზანია დიდი ენობრივი მოდელებისთვის (LLMs) ფორმალური დამტკიცების ამოცანების გადაჭრა ასწავლოს, რაც დაგეგმვისა და შესრულების გამიჯვნის ხარჯზე ზრდის ახსნადობას,