📌 Palomar - реестр проверенных LEAN-доказательств Последние месяцы доказательства, сгенерированные ИИ, посыпались валом как для новых результатов, так и для старых, причем часть из них формализована на Lean и проверить такой репозиторий непросто, особенно если ты не эксперт. Нужно убедиться: 🟠что заявленные формальные утверждения действительно имеют доказательства, проходящие проверку типов; 🟠что в доказательствах нет жульничества; 🟠что формальные утверждения по смыслу совпадают с тем, что описано словами. Под эту задачу и Теренс Тао запустил Palomar - реестр математики, верифицированной на Lean. Инициативу вырастили Lean FRO и ICARM. Прием заявок уже идет, чтобы в него попасть, в репозитории должно быть три вещи: 🟢challenge file с коротким и читаемым человеком описанием заявленных результатов на Lean; 🟢solution module с доказательством любой длины; 🟢файл formalization.yaml, где те же результаты изложены обычным языком и собраны метаданные и раскрытия. Снимок поданного репозитория проверяют двумя этапами. Сначала инструмент Comparator смотрит, что solution module типизируется и доказывает ровно то, что заявлено в challenge file. После этого языковая модель сверяет, похоже ли неформальное описание в на то, что заявлено формально. Прошел оба - попал в реестр. Принимают формализации и старых результатов, и новых. Кто автор доказательства - человек, ИИ или оба вместе - значения не имеет. @ai_machinelearning_big_data #news #ai #ml

Недавно мы в институте провели семинар об ИИ в математике с потрясающими приглашёнными спикерами: - Легендарный Дмитрий Рыбин рассказал об агентах для совершения открытий и сложных задач - Невероятный Василий Ильин рассказал об автоматической и надёжной формализации математики, а также провёл ликбез, что вообще такое формализация и Lean Мы в основном занимаемся биологией, поэтому спикеры подготовили доклады, которые понятны даже нематематикам. ИИ очень сильно меняет эту область уже сегодня, но это вскоре случится и с другими науками. Если хотите раньше других увидеть, как этот процесс выглядит изнутри, смотрите запись семинара Спикеры буквально находились на противоположных частях земного шара, а семинар проводился совсем в другом месте. Просто чудо, что всё удалось организовать без проблем. Обычно этот семинар внутренний, но получилось так здорово, что решили сделать запись доступной всем. Это немало работы, поэтому буду очень благодарен за лавки и репосты! #математика@chelovek_nauk

🌟 Mistral AI обновила модель Leanstral Leanstral 1.5 - новая версия ранее выпущенной модели для формальной верификации в языке Lean 4. Задача подобных моделей помогать составлять и проверять доказательства, которые компилятор Lean принимает как корректные.

Lean 4 - это система интерактивного доказательства теорем, которая позволяет записывать математические утверждения и проверять их строго формально, а также описывать свойства программного кода.

Обновление не затронуло изменение архитектуры, количество параметров и окно контекста, под капотом также MoE на 119 млрд общих и 6,5 млрд активных параметров, 256 тысяч токенов контекст и мультимодальность на входе. Версия 1.5 прошла техэтапное обучение в 2-х средах: одна отрабатывает доказательство теорем в диалоге с компилятором Lean, другая учит модель действовать как программист в реальных репозиториях. 🟡Тесты Апдейт полностью насыщает бенчмарк miniF2F, набирая 100% на проверочной и тестовой выборках, решает 587 из 672 задач PutnamBench и показывает лучшие на сегодня результаты на наборах FATE-H и FATE-X.

К слову, на PutnamBench, Leanstral 1.5 опережает систему Seed-Prover 1.5 на 7 задач при затратах около 4 долларов на задачу (против 300+ долларов у соперника).

В тесте по кодингу на 57 репозиториях, система с участием Leanstral выявила 47 нарушенных свойств, из которых 11 оказались реальными ошибками, а 5 ранее не были известны. 📌Лицензирование: Apache 2.0 License 🟡Блогпост 🟡Модель 🟡Demo @ai_machinelearning_big_data #AI #ML #LLM #LEAN #LeanStral #MistralAI