В одном интервью World Science Festival от 2 октябряматематик Тристан Бакмастер рассказал о результате, полученном с помощью ИИ: он считает его верным, но трудным для чтения другими математиками. Его рассказ ставит более конкретный вопрос после недавнего заявления о Навье–Стоксе: как научное сообщество может проверить формальный аргумент, если для понятного объяснения нужна дополнительная работа?

Бакмастер говорил о своей работе с Левентом Алпёге над трёхмерными уравнениями Эйлера с гладкой внешней силой. Их результат отличается от заявления OpenAI от 8 сентября об уравнениях Навье–Стокса с гладкой внешней силой. В уравнениях Навье–Стокса учитывается вязкость, в уравнениях Эйлера — нет. OpenAI опубликовала статью и формализацию в Lean для заявленного результата о потере гладкости за конечное время. Учреждение, управляющее Millennium Prize, не объявляло о присуждении награды.

Большое изменение

  • Что изменилось: Бакмастер поделился личным опытом применения аргументов, созданных ИИ, и Lean для доказательства отдельного результата для уравнений Эйлера с внешней силой, а также рассказал, какая работа ещё нужна, чтобы объяснить такие доказательства математикам.
  • Почему это важно:Формальная проверка может установить, что закодированный аргумент следует из заданных определений и зависимостей. Математикам также нужно понимать, что утверждает теорема, как работают её идеи и на чьих прежних результатах она основана.
  • За чем следить:Оценка Clay заявления OpenAI о Навье–Стоксе, понятные изложения доказательства и публичное обсуждение авторства и доступа покажут, как оценивают этот результат. Уверенность Бакмастера в результате — экспертное мнение, а не решение о присуждении премии.

Даже проверенному аргументу нужно объяснение

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

Различие имеет практическое значение. Lean проверяет точно формализованное утверждение в заданной среде доказательства. Сам по себе он не делает длинный аргумент понятным исследователю, который хочет повторно использовать его метод. Бакмастер рассказал Брайану Грину, что другие системы ИИ могли разбирать фрагменты, которые он едва мог прочитать, а просьба перевести их на обычный математический язык стала частью работы. Он также сказал, что всё ещё понимает идеи аргумента о Навье–Стоксе, хотя опубликованный PDF трудно читать. Это его оценки, а не проверка доказательств со стороны BIG CHANGE; мы не запускали файлы Lean и не рецензировали ни одну из теорем.

В отчёте NYU Courant от 14 сентября достижение Бакмастера и Алпёге описано как потеря гладкости за конечное время для уравнений Эйлера с внешней силой в трёх измерениях, гладкой силой и начальными данными с конечной энергией. В отчёте говорится, что три совместные статьи формализованы в Lean, а результат продолжает направление, начатое Диего Кордовой и Луисом Мартинесом-Сороа. Эти детали важны при распределении заслуг: созданное моделью доказательство может развить существующий математический подход, не стирая вклад людей, которые его заложили.

Два результата в быстро развивающейся последовательности

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

Европейское математическое общество приветствовало объявление, одновременно подчеркнув значение прежних работ и призвав уделить внимание авторству, заслугам и доступу к внутренней модели. В ответе Clay от 11 сентября говорилось, что задача Навье–Стокса по-видимому решена, а оценку достижения и распределение заслуг не следует торопить. Бакмастер сказал Грину, что верит в наличие решения у OpenAI. Эти два утверждения могут сосуществовать: положительная оценка специалиста и продолжающаяся проверка со стороны учреждения.

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

Для столь значимого утверждения следующими полезными публикациями станут точные, понятные изложения, проверяемые формальные артефакты и независимые математические отклики. Каждая выполняет свою задачу. Скорость создания кандидата на доказательство делает эти задачи более срочными, а заявленная процедура Clay оставляет время для тщательной работы.

Источники и дополнительная литература