**📌****Mistral AI випустила Leanstral 1.5 для формальної верифікації**

Mistral AI оновила Leanstral — спеціалізовану модель для роботи з мовою Lean 4, яка використовується для формального доведення теорем і перевірки коректності програм. Версія 1.5 отримала новий етап навчання та значно покращила результати на профільних бенчмарках.

🔆**Детальніше**

• Призначена для формальної верифікації математичних доведень і програмного коду в Lean 4.

• Зберегла архітектуру MoE: 119 млрд загальних і 6.5 млрд активних параметрів.

• Має контекстне вікно 256 тисяч токенів і підтримує мультимодальний вхід.

• Навчалася у двох середовищах: для взаємодії з компілятором Lean та роботи з реальними репозиторіями коду.

• Досягла 100% на miniF2F, розв'язала 587 із 672 задач PutnamBench та показала найкращі результати на FATE-H і FATE-X.

• Поширюється за ліцензією Apache 2.0.

➡️Нuggingface [тут](/leaving?url=aHR0cHM6Ly9odWdnaW5nZmFjZS5jby9taXN0cmFsYWkvTGVhbnN0cmFsLTEuNS0xMTlCLUE2Qg==).
➡️Спробувати [тут](/leaving?url=aHR0cHM6Ly9jb25zb2xlLm1pc3RyYWwuYWkvYnVpbGQvcGxheWdyb3VuZA==).
➡️Детальніше [тут](/leaving?url=aHR0cHM6Ly9taXN0cmFsLmFpL25ld3MvbGVhbnN0cmFsLTEtNS8=).

➡️**_Запроси друга до _**[**_НейроЄнота_**](https://t.me/neuroenot)🦝