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

Источник: devby.io

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

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

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

Руководитель научной группы «Методы оптимизации в машинном обучении» Института AIRI Александр Тюрин признался: «Фреймворк за пару дней доказал больше результатов, чем я сам за всю свою карьеру. Сложно определиться, как я к этому отношусь, но это очень интересно». По его словам, исследователи продолжат доказывать новые теоремы, повышать сложность задач, структурировать их и добиваться, чтобы найденные алгоритмы были эффективны на практике. Код исследования выложен в открытый доступ, и им могут воспользоваться другие научные группы.