OpenAI выложила на GitHub 372 математических доказательства, призвав академический мир не отставать

OpenAI выпустила большую коллекцию математических результатов, созданных внутренней моделью ИИ. Доказательства опубликованы на GitHub, а не в научных журналах; формальная верификация должна сделать их проверку более практичной.

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

Компания разместила результаты в репозитории GitHub с журналами изменений и ссылками на источники. По данным OpenAI, та же модель уже предложила решение задачи Навье — Стокса, которая в течение нескольких недель находилась на формальной проверке.

OpenAI сообщает, что почти каждый результат был получен с помощью одного запроса к одному ИИ-агенту, хотя для некоторых потребовалось несколько попыток. Это резко контрастирует с решением задачи Навье — Стокса, для которого потребовался рой из 10 000 агентов и вычисления стоимостью в миллионы долларов. В среднем на каждый результат уходило примерно три часа вычислений в режиме размышлений ChatGPT Pro.

Формальная верификация может ослабить узкое место в процессе проверки

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

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

Традиционные журналы не рассчитаны на такие темпы

OpenAI разместила свои результаты на GitHub, а не в рецензируемых журналах. Это символичный шаг, поскольку он подразумевает, что традиционный научный процесс слишком медленный для такого объёма потенциально новых знаний.

OpenAI консультировалась с Консультативной группой по математике и искусственному интеллекту при Институте перспективных исследований и в общих чертах следовала её публичным рекомендациям, поскольку компания не опубликовала запросы и поделилась лишь средними вычислительными затратами, а не показателями по каждой задаче. В состав консультативной группы, помимо других известных математиков, входит лауреат Филдсовской премии Тимоти Гауэрс.

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

Однако заранее OpenAI установила для консультативной группы одно существенное ограничение: математики могут давать советы о том, как сообщать о результатах, но не о том, создавать ли их и с какой скоростью.

Математическое сообщество разделилось во мнениях о значении массового производства доказательств

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

В недавнем открытом письме под названием «Серьёзное рассогласование ИИ с математикой» 25 лауреатов Филдсовской премии предупредили о глубоком разрыве между целями индустрии ИИ и целями математики. Решение задач, писали они, является лишь инструментом и заменителем настоящей цели — концептуального понимания и озарения. По их мнению, массовое производство истинных утверждений может уничтожить плодородную почву, а не породить новые идеи. Последствия распространятся и на другие области.

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

Новости ИИ без шумихи — отобраны людьми

Подпишитесь на THE DECODER и получите чтение без рекламы, еженедельную рассылку об ИИ, наш эксклюзивный передовой отчёт «AI Radar» шесть раз в год, полный доступ к архиву и доступ к разделу комментариев.