Поддержать
Вскоре после предыдущего прорыва в области математики компания OpenAI представила результаты работы новой модели Astra, которая, по данным компании, решила десять открытых математических задач, остававшихся нерешенными на протяжении десятилетий. Все полученные доказательства сопровождаются машинной проверкой в системе Lean и находятся в открытом доступе. Исследователи называют это важным шагом для использования искусственного интеллекта в науке, хотя часть экспертов призывает не торопиться с выводами, передает Forbes.
По оценке OpenAI, стоимость получения этих результатов составила около 2000 долларов. Работа была опубликована 1 августа вместе с 249-страничным сборником решений. Главной особенностью проекта стали машинно проверенные сертификаты для каждого результата, которые OpenAI опубликовала в открытом доступе на GitHub.
По данным компании, все доказательства формализованы в системе Lean — программном помощнике для проверки математических доказательств. Любой желающий может скачать файлы и проверить их: если хотя бы один шаг логической цепочки является неверным, программное обеспечение автоматически отклоняет доказательство.
Astra решила десять сложных математических задач из различных областей, в частности теории групп, гиперболической геометрии, теории кодирования, квантовой сложности, криптографии на решетках и экстремальной комбинаторики. Среди полученных результатов — построение конструкции, подтверждающей существование несофических групп, решение проблемы, связанной с гипотезой жесткости Коннеса, улучшение верхней границы плотности упаковки сфер в высоких измерениях, которая оставалась неизменной с 1978 года, а также три задачи из известного каталога открытых проблем, составленного математиком Полом Эрдешем.
Это уже второй громкий результат модели Astra. В мае OpenAI сообщала, что она опровергла гипотезу о единичном расстоянии Эрдеша — задачу дискретной геометрии, которая оставалась нерешенной около 80 лет.
Результаты положительно оценили ряд известных математиков. Лауреат медали Филдса Тим Говерс заявил, что без колебаний рекомендовал бы эти доказательства к публикации в ведущем математическом журнале, а впоследствии вместе с восемью коллегами, среди которых был Нога Алон, подготовил отдельную статью с объяснением доказательств в более доступной для математиков форме. Томас Блум, ведущий каталог задач Эрдеша, назвал августовские результаты «великой новостью» и отметил, что они могут оказаться даже более важными, чем предыдущий результат по гипотезе единичного расстояния.
В то же время публикация не обошлась без критики. Эксперты обращают внимание на то, что именно OpenAI выбирала, какие результаты обнародовать, а заявленная сумма в 2000 долларов касается только успешных запусков модели, а не всех попыток получить правильный результат.
Кроме того, исследователи отмечают, что сотрудники OpenAI участвовали в подготовке научных статей и формализации доказательств. Также модель Astra пока недоступна сторонним исследователям, поэтому независимо воспроизвести процесс получения результатов невозможно — можно лишь проверить уже опубликованные доказательства.
Один из самых известных критиков современного ИИ Гэри Маркус назвал релиз «удивительным, но чрезвычайно переоцененным». Часть математиков также считает, что после более детального анализа не все десять задач будут иметь одинаковый научный вес.
Несмотря на это, опубликованные машинно проверенные сертификаты меняют сам подход к оценке результатов ИИ. Если раньше научное сообщество было вынуждено доверять заявлениям разработчиков моделей, то теперь правильность математических доказательств можно независимо проверить автоматически.
В OpenAI считают, что такая схема может иметь значение далеко за пределами математики. Подобные механизмы уже используются при проектировании микросхем, в криптографии, проверке аппаратного обеспечения и критически важного программного обеспечения, где возможность автоматически подтвердить правильность результата часто важнее скорости его получения.
Между тем в области математики не отстают и модели компании Anthropic. Искусственный интеллект Claude Fable 5 в сотрудничестве с учёными нашёл вероятный контрпример к гипотезе Якобиана, которая остаётся нерешённой с 1939 года. Модель сгенерировала математическую конструкцию, нарушающую условия глобальной обратимости полиномиального отображения, но эта работа ещё ожидает официального рецензирования и публикации.
Следить в Телеграмме
Войти с помощью Facebook
Войти с помощью Twitter
Войти с помощью Google