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