Mistral-მა 2 ივლისს გამოუშვა Leanstral 1.5 — Lean 4-ში ფორმალური ვერიფიკაციისთვის შექმნილი უფასო და ღია კოდის AI მოდელი, რომელიც დეველოპერებს და მათემატიკოსებს საშუალებას აძლევს, მკაცრი მათემატიკური მეთოდებით დაამტკიცონ პროგრამული კოდის სისწორე და ამოხსნან კომპლექსური თეორემები — ამოცანაზე დაახლოებით $4-ად, კონკურენტ სისტემებში კი ეს ხარჯი $300-ს ან მეტს შეადგენს.
მოდელი იყენებს mixture-of-experts არქიტექტურას 119 მილიარდი მთლიანი პარამეტრით, სადაც გაშვებისას მხოლოდ 6 მილიარდია აქტიური — ეს მას ჩვეულებრივ ტექნიკაზე ეფექტური გამოყენების საშუალებას აძლევს. Mistral-მა მოდელი სამ ეტაპად მოამზადა: mid-training, supervised fine-tuning და CISPO-ს გამოყენებით reinforcement learning — ორ გარემოში: მრავალბიჯიანი თეორემების დამტკიცების სიმულაციაში და კოდის აგენტის გარემოში, სადაც ნამდვილი ფაილური სისტემის ოპერაციები სიმულირდება.
ბენჩმარქები
Leanstral 1.5 პირველი საჯაროდ ხელმისაწვდომი მოდელია, რომელმაც სრულად გაჯერა miniF2F — თეორემების დამტკიცების სტანდარტული ბენჩმარქი — ვალიდაციის და ტესტის ნაკრებებზე 100%-ის შედეგით. PutnamBench-ზე — William Lowell Putnam Mathematical Competition-ის ამოცანებიდან შემდგარ ბენჩმარქზე — მოდელმა 672-დან 587 ამოხსნა. FATE-H-ზე 87% და FATE-X-ზე 34% — ორივე შემთხვევაში საუკეთესო შედეგი.
ხარჯთეფექტურობის სხვაობა მნიშვნელოვანია: Mistral-ის მონაცემებით, Leanstral 1.5 ამოცანას ამოხსნის დაახლოებით $4-ად, მაშინ როდესაც კონკურენტ სისტემებში ეს ხარჯი $300-ს ან მეტს შეადგენს.
პრაქტიკული შედეგები
ბენჩმარქებს გარდა, Mistral-მა Leanstral 1.5 57 ღია კოდის რეპოზიტორიაზე გაუშვა და ხუთი ადრე უცნობი შეცდომა აღმოაჩინა, მათ შორის Rust ბიბლიოთეკის zigzag-კოდირების ფუნქციაში კრიტიკული მთელი რიცხვის გადაფარვა. უფრო ვრცელ ამოცანაში კი მოდელმა 2.7 მილიონი ტოკენის გამოყენებით AVL ხის ოპერაციებისთვის O(log n) სირთულე დაამტკიცა.
ხელმისაწვდომობა
მოდელის წონები Hugging Face-ზეა Apache-2.0 ლიცენზიით. Mistral-ის პლატფორმაზე ხელმისაწვდომია უფასო API ენდფოინთი (leanstral-1-5), Mistral Vibe-ის ინტეგრაციით. კომპანიის ინფორმაციით, უფასო ენდფოინთი 2026 წლის 30 სექტემბრამდე იმუშავებს.