📌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 тут.
➡️Спробувати тут.
➡️Детальніше тут.
➡️Запроси друга до НейроЄнота🦝
📌Mistral AI випустила Leanstral 1.
Нейроєнот | Нейромережа Midjourney, chat GPT та інші
@neuroenotЗахопливо про нейромережі та проривні технології. Ласкаво просимо у майбутнє. #добірка - добірка всіх новин за тиждень Для друга: https://t.me/neuroenot Співпраця та зв'язок: @New_Life_Technology
14,339 subscribers
Open in Telegram 4 photos are attached to this post — visible in the Telegram app.