Скор на разгадку: новый ИИ-агент докажет теоремы в разы быстрее математиков

Российские ученые создали систему, которая самостоятельно формулирует задачи математической оптимизации, подбирает методы их решения и формально доказывает полученные результаты. С ее помощью удалось сформулировать около 100 теорем, 35 из которых получили доказательства. На доказательство одной теоремы ИИ в среднем требуется от трех до семи часов — это в разы быстрее, чем у профессиональных математиков. Однако использование платформы несет и определенные риски. В частности, система может выдавать корректные ответы на некорректно сформулированные задачи, предупредили эксперты. Сможет ли алгоритм заменить ученых в отдельных операциях — в материале «Известий».

От перебора методов до доказательства

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

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

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

Фото: Global Look Press/Razmik Zackaryan/URA.RU

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

Риски применения платформы

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

— Если постановку задачи сформулировал агент, ошибка может быть заложена уже на этом этапе. Тогда безупречное доказательство подтверждает неверный результат. Поэтому ответственность за то, что именно доказано и где это применяется, остается на исследователе, — отметила советник практики интеллектуальной собственности ЮК «ЭБР» Ольга Яшина.

Другой эксперт обращает внимание на различие между формальной корректностью и научным пониманием. По словам основателя финтех-платформы SharesPro Дениса Астафьева, доказательство может быть безупречным с точки зрения математики, но практически недоступным для человеческого понимания. Для развития науки этого недостаточно: исследователь должен понимать, почему работает найденный метод и как его можно применять в других задачах.

— Способность машины самостоятельно получать математически корректные результаты ставит вопрос о том, насколько такие исследования зависят от человеческого понимания, — пояснил он.

Фото: Global Look Press/Artur Cupak/imageBROKER.com

Перспективными могут стать системы, которые способны не только выдавать доказательство, но и объяснять ход рассуждений. В противном случае машина решает конкретную математическую задачу, но не обязательно дает человеку новое понимание, пояснил ведущий разработчик MWS AI Cowork Егор Старовойтов.

Основная трансформация будет связана с перераспределением функций. ИИ возьмет на себя все больше вычислений и технического поиска, тогда как специалисту останутся постановка исследовательских задач, построение моделей и оценка научной значимости результатов, полагает заведующий кафедрой теории и методики компьютерного спорта, шахмат и цифровых технологий РУС «ГЦОЛИФК» Михаил Новоселов.

— Здесь возникает и образовательный риск. Если постоянно передавать ИИ сложные этапы рассуждений, молодые исследователи могут получить меньше практики самостоятельного построения доказательств. Поэтому обучение должно сочетать работу с ИИ и самостоятельное решение математических задач, — пояснил доцент Финансового университета при правительстве РФ Артур Вафин.

Фото: ИЗВЕСТИЯ/Сергей Лантюхов

Оснований говорить о массовом неприятии подобных технологий среди математиков нет. Как отметил заместитель руководителя направления «Искусственный интеллект» ИТ-холдинга Т1 Евгений Григорьев, ИИ способен взять на себя значительную часть рутинной работы — поиск и проверку доказательств, перебор подходов и технические вычисления. Это позволяет ученым сосредоточиться на более сложных задачах.

Математики будут нужны и дальше

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

— Технологический прогресс в данном случае повышает требования к человеку, а не отменяет его роль. Исследователь должен будет определять, какие из множества возможных задач действительно представляют научную ценность, и контролировать применение полученных результатов, — отметила политолог Елена Штульман.

Фото: ИЗВЕСТИЯ/Сергей Лантюхов

С развитием ИИ профессия математика будет меняться — как содержание работы, так и направления применения полученных знаний, считает руководитель команды ИИ-тренеров модели Alice AI по высшей математике Ашот Маргарян.

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

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