Специалисты Института AIRI и их коллега из Вьетнама представили LongTails — открытый фреймворк, в котором ИИ сам ставит задачи математической оптимизации, ищет способы их решения и строго обосновывает полученный ответ. Об этом сообщает портал Компьютерра.
Всего за несколько дней система сформулировала и формализовала порядка ста теорем. Для 50 из них гарантии оказались лучше, чем в более ранних работах. Ещё 35 результатов авторы намерены издать отдельно: по их оценке, они заслуживают публикаций в международных журналах. На одну теорему у агента уходит от трёх до семи часов.
Ключевое отличие LongTails — автоматическая проверка доказательств на языке формальной верификации Lean 4. Так снимается главная сложность применения ИИ в математике: модель может выдать правдоподобное рассуждение с ошибкой или обосновать совсем другую задачу. Система опирается на формально записанные условия и цель, поэтому каждый её результат гарантированно верен.
Методы оптимизации ищут лучшее решение среди множества вариантов — самое быстрое, дешёвое, точное или надёжное. Доказываемые теоремы описывают, при каких условиях и насколько быстро работает конкретный метод. Эти гарантии дают возможность заранее оценить объём вычислений и выбрать алгоритм, а не перебирать их вслепую.
Подобные алгоритмы лежат в основе обучения нейросетей — от рекомендательных сервисов до больших языковых моделей. Их эффективность сокращает время тренировки, расходы на вычисления и энергопотребление дата-центров. Кроме того, они помогают проектировать лёгкие и прочные конструкции, прокладывать маршруты доставки, распределять нагрузку в электросетях, искать молекулы и материалы, обрабатывать данные физических экспериментов и управлять инвестиционными рисками.
Код исследования открыт, им могут воспользоваться другие научные группы. «Фреймворк за пару дней доказал больше результатов, чем я сам за всю свою карьеру. Сложно определиться, как я к этому отношусь, но это очень интересно», — рассказал Александр Тюрин, руководитель группы, занимающейся оптимизацией в машинном обучении в Институте AIRI. По его словам, работа продолжится: сложность задач будут повышать, а найденные алгоритмы предстоит довести до практической эффективности.