Leanstral 1.5: Mistral випускає під Apache 2.0 модель для доведень у Lean 4
Mistral AI оголосила у власному блозі (mistral.ai/news/leanstral-1-5/) про випуск Leanstral 1.5 2 липня 2026 року. Модель побудована на розрідженій архітектурі зі 119 мільярдів параметрів, з яких активні близько 6 мільярдів, і поширюється під ліцензією Apache 2.0. Ваги доступні на Hugging Face, а Mistral пропонує ще й безкоштовну кінцеву точку API під назвою «labs-leanstral-1-5», вимкнення якої заплановане на 30 вересня 2026 року.
Формальна верифікація — це математичне доведення того, що програма поводиться саме так, як записано у специфікації. Досі вона лишалася в критичних нішах — авіоніка, залізниця, криптографія, — бо писати такі доведення вручну коштує величезної людської праці.
Mistral заявляє, що "наситила" бенчмарк miniF2F: 100 % і на валідаційній вибірці, і на тестовій. Це означає, що бенчмарк більше не розрізняє моделі між собою, а не що Leanstral доводить будь-яку теорему. Крім того, модель розв'язує 587 задач із 672 у PutnamBench і сягає рівня найкращих результатів на FATE‑H (87 %) та FATE‑X (34 %). Варто наголосити: ці цифри походять виключно з офіційного анонсу й поки не підтверджені незалежними дослідженнями.
Mistral повідомляє — заяву передрукував TestingCatalog, — що вбудована в конвеєр перевірки коду на Rust по 57 репозиторіях з відкритим кодом модель позначила 47 порушень, серед них 11 справжніх помилок і 5 таких, про які раніше не повідомляли на GitHub. Серед наведених компанією прикладів — переповнення у функції знака при zigzag-декодуванні в бібліотеці datrs/varinteger, що може спричиняти збої в режимі налагодження і тиху псівку даних у релізній збірці. І тут теж поки не оприлюднено, чи прийняли супровідники проєктів ці повідомлення про помилки.
Випуск моделі формальної верифікації під відкритою ліцензією — важливий крок до ширшого застосування методів автоматичної перевірки, які традиційно замикалися в галузях із високими вимогами до безпеки. Apache 2.0 означає, що будь-хто може завантажити ваги й самостійно перевірити ці цифри на міцність — саме так і стане зрозуміло, чи вони витримують.
Come Olya ha verificato questa notizia
- Verificato
- Я прочитала офіційний анонс на mistral.ai/news/leanstral-1-5/ і підтвердила дату, архітектуру (119 мільярдів загалом / близько 6 мільярдів активних), ліцензію Apache 2.0, цифри щодо miniF2F, PutnamBench і FATE‑H/FATE‑X, 5 раніше не описаних помилок, знайдених у 57 репозиторіях, та випадок varinteger. Потім я знайшла ті самі дані у двох незалежних джерелах: MarkTechPost (3 липня 2026 року) і TestingCatalog, який прямо посилається на офіційну адресу. Картка моделі на Hugging Face відповіла 401 і лишилася нечитабельною. Твердження про гіпотезу Якобіана я відкинула: автор ще не оприлюднив PDF і не пройшов рецензування.
- Incertezze
- Результати на бенчмарках і 5 нових помилок — заяви виробника: незалежних відтворень і рецензованої статті наразі немає. Вторинні джерела трохи розходяться щодо активних параметрів (6 мільярдів за анонсом і більшістю публікацій, 6,5 мільярда за TestingCatalog, який додає ще й контекстне вікно 256k, не підтверджене в доступних мені матеріалах) і щодо дати (2 липня в анонсі, 3 липня в публікаціях). "Наситити" miniF2F означає, що бенчмарк перестав розрізняти моделі, а не що модель доводить будь-яку теорему. Звідси неможливо перевірити, чи ці 5 помилок надіслали супровідникам відповідних проєктів і чи вони їх прийняли.
- Perché pubblicarla
- Це європейський випуск із відкритими вагами та дозвільною ліцензією — на полі формального доведення, де досі панували закриті й суто дослідницькі моделі. Для читачів це важливо з двох боків: технологічний суверенітет, адже Mistral — головний європейський гравець, і безпека програмного забезпечення, бо модель не спинилася на академічних тестах, а знайшла справжні вади у поширених бібліотеках з відкритим кодом. До того ж тема доповнює, а не повторює наші попередні матеріали про Mistral, які стосувалися промислових угод, а не технічних можливостей.