OpenAI опубликовала результаты внутренней экспериментальной ИИ-модели, вызвав оживлённые споры среди математиков о методах проверки и включения таких работ в научное знание.
В репозиторий вошли 722 работ, сгруппированные в 372 набора связанных результатов по чистой математике, теоретической информатике и математической физике. Модель проверили на 4000 задачах. Для многих работ "Астра" подготовила формальные доказательства на языке Lean для автоматической проверки на логическую корректность, но не все материалы были ещё проверены.
Публикация последовала за сентябрьским заявлением OpenAI о решении одной из задач тысячелетия — о существовании и гладкости уравнений Навье — Стокса. GPT Astra получила доказательство возникновения сингулярности в трёхмерном течении при определённых условиях. Вместе с обычным изложением компания опубликовала формализацию доказательства в Lean. Однако официальное признание результата ещё не завершено, и Clay Mathematics Institute подтвердил, что оценка таких работ требует времени.
Быстрый прогресс ИИ в математике поднял вопрос о публикации результатов, которые ещё не получили полного человеческого объяснения. Независимая Консультативная группа по математике и искусственному интеллекту при Институте перспективных исследований в Принстоне заявила, что понимание доказательств людьми должно оставаться важным.
Группа выступила против использования закрытых моделей для массового решения сложных задач без доступа к ним для научного сообщества. Это может привести к тому, что частные лаборатории будут опережать независимую математическую науку.
Рекомендации касаются правил публикации, а не запрета ИИ в математике. Если результат ещё не полностью понят, лаборатории должны публиковать подробное описание метода, используемые запросы, информацию о вычислительных затратах, статус формальной проверки и ссылки на предыдущие работы.
Также важно, чтобы компании, занимающиеся ИИ-математикой, поддерживали независимые семинары и программы для разбора доказательств.
OpenAI частично следует этим рекомендациям, опубликовав историю версий работ, формализации Lean, статистику по 4000 задачам и описания процесса решения. Компания также объявила о планах финансировать конференции и семинары для изучения крупных результатов ИИ. Независимая группа подчёркивает, что консультации с OpenAI не являются одобрением всех опубликованных материалов. Окончательную оценку их значения должно дать математическое сообщество.
Возникает вопрос научного авторства. ИИ обучаются на существующих работах и могут продолжать идеи, разработанные людьми, поэтому важно отслеживать происхождение методов и правильно указывать предыдущие результаты.
Спор усилился после работы над задачей Навье — Стокса. Тристан Бакмастер, математик из Нью-Йоркского университета, выразил опасения, что закрытые ИИ-системы могут использовать идеи из ещё не опубликованных исследований. OpenAI заявила, что запросы Бакмастера не могли повлиять на модель, использованную для доказательства.
Текущая публикация показывает, что проблема выходит за рамки одной задачи. Если первые ОИИ способны работать с тысячами математических вопросов и выдавать сотни новых результатов, основной труд будет смещаться от получения доказательств к их проверке и объяснению. Поэтому важно не только оценить силу математических моделей, но и способность людей понять, проверить и развить результаты.