Агент LongTails института AIRI доказал более 30 новых теорем оптимизации

Проверка в Lean 4

Главная особенность LongTails — автоматическая проверка каждого доказательства на языке формальной верификации Lean 4. Это защита от известной проблемы применения ИИ в математике: модель может выдать убедительное на вид рассуждение, в котором есть ошибка или которое решает не ту задачу. Система исходит из формального описания условий и цели, а затем проверяет, соответствует ли им доказательство.

Исследователи получили около 100 формально записанных теорем, из них 50 улучшают гарантии, известные из прежних работ. Еще 35 теорем команда намерена опубликовать как самостоятельные математические результаты, достойные международных публикаций. На доказательство одной теоремы программа тратит в среднем от 3 до 7 часов.

Практическое значение

Оптимизация — это поиск наилучшего варианта среди множества возможных: самого быстрого, дешевого или точного. Доказанные теоремы показывают, насколько быстро работает метод и при каких условиях, что позволяет заранее оценить число нужных вычислений. Обучение нейросетей, от рекомендательных систем до больших языковых моделей, опирается на методы оптимизации, поэтому более эффективные алгоритмы могут сократить время обучения, затраты и энергопотребление дата-центров. Те же методы применяют при проектировании легких и прочных конструкций, планировании маршрутов доставки, распределении нагрузки в энергосетях, поиске новых молекул и материалов и управлении инвестиционными рисками.

Код LongTails открыт, и другие научные группы могут им пользоваться. Один из участников проекта рассказал, что за несколько дней фреймворк достиг большего, чем он сам за всю карьеру, и ему трудно описать свои чувства, но он находит это крайне увлекательным. Команда продолжит доказывать новые теоремы, усложнять и упорядочивать задачи, а также проверять найденные алгоритмы на практике.