ИИ OpenAI выдаёт математические результаты быстрее, чем учёные успевают их проверять

OpenAI опубликовала сотни математических результатов, полученных внутренней экспериментальной ИИ-моделью, и одновременно вызвала дискуссию среди математиков о том, как такие работы должны проверяться и включаться в научное знание. В открытый репозиторий вошли 722 рукописи, объединённые в 372 семейства связанных результатов по чистой математике, теоретической информатике и математической физике.

Модель проверяли примерно на 4000 исследовательских задачах. Для многих опубликованных работ OpenAI также подготовила формальные доказательства на языке Lean, которые можно автоматически проверить на логическую согласованность, однако такая проверка есть не у всех материалов.

Публикация последовала за сентябрьским заявлением OpenAI о решении задачи существования и гладкости уравнений Навье — Стокса — одной из семи задач тысячелетия. Внутренняя система компании получила доказательство, согласно которому гладкое трёхмерное течение при определённых условиях может за конечное время развить сингулярность; вместе с обычным изложением OpenAI опубликовала формализацию доказательства в Lean.

При этом официальное признание результата ещё не завершено. Clay Mathematics Institute 11 сентября сообщил, что задача «по-видимому, решена», но подчеркнул, что оценка подобных результатов проводится по установленной процедуре и требует времени. На странице самой задачи Навье — Стокса она по-прежнему обозначена как активная.

Быстрый прогресс ИИ в математике вызвал отдельный спор о том, как должны публиковаться результаты, которые ещё не получили полного человеческого объяснения. Независимая Консультативная группа по математике и искусственному интеллекту при Институте перспективных исследований в Принстоне заявила, что человеческое понимание доказательств должно оставаться важной частью математической науки.

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

Рекомендации касаются не запрета ИИ в математике, а правил публикации. Если результат ещё никто из людей полностью не понимает, лаборатории предлагается публиковать максимально полное описание метода, используемые запросы, сведения о вычислительных затратах, статус формальной проверки и ссылки на связанные предыдущие работы.

Отдельное требование связано с человеческим осмыслением новых доказательств. Консультативная группа считает, что компании, выпускающие большие объёмы ИИ-математики, должны поддерживать независимые семинары, рабочие группы и другие программы, в которых специалисты смогут разбирать доказательства и включать их в существующую математическую теорию.

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

При этом независимая группа подчёркивает, что её консультации с OpenAI нельзя считать одобрением всех опубликованных результатов или самого способа их получения. После релиза 6 октября она заявила, что публикация материалов — только начало процесса и окончательную оценку их значения должно дать математическое сообщество.

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

Спор усилился после работы над задачей Навье — Стокса. Математик Нью-Йоркского университета Тристан Бакмастер ранее выражал опасения, что закрытые ИИ-системы могут использовать идеи, близкие к ещё не опубликованным исследованиям. OpenAI заявила после внутренней проверки, что запросы Бакмастера в Codex не могли повлиять на модель, использованную для доказательства, в том числе через обучение.

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

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