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

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

«Просто просмотр всего списка аннотаций ошеломляет», — сказал Альваро Лосано-Робледо, профессор математики в Университете Коннектикута. Несколько математиков сообщили The Verge, что только на изучение примерно 40-страничного оглавления и аннотаций у них ушло больше часа. Для тех, кто считает дома: это час только на чтение меню.

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

Но степень проверки каждого результата сильно различалась. На GitHub OpenAI признала, что результаты находятся «на разных стадиях верификации» и что «многие, но не все рукописи были формализованы». На момент написания менее половины рукописей в коллекции, по-видимому, были описаны формально. OpenAI заявила, что только 300 ключевых результатов из 719 рукописей были формализованы — около 42% — и что она «будет обновлять репозиторий новыми формализациями по мере их получения». Итак, примерно 58% математического апокалипсиса остаются непроверенными. Спите спокойно.

Несколько математиков пожаловались The Verge на недостаток формализации, особенно учитывая огромное количество результатов. Даже когда код на Lean сопровождает результат, оценка не происходит мгновенно. Исследователи должны проверить, что формализация действительно доказывает то, что утверждает результат — ещё один трудоёмкий процесс. Несколько человек, изучавших статьи, сказали, что даже там, где были предоставлены проверяемые компьютером доказательства, качество было неоднородным, и утверждения, которые они проверяли, не всегда, по-видимому, точно соответствовали заявлениям в сопроводительных рукописях.

Кевин Баззард, профессор математики в Имперском колледже Лондона, сказал, что выявил множество теорем в своей области — алгебраической теории чисел — из которых только около шести сразу «бросались в глаза». Мало какие из них, если вообще какие-либо, были формально проверены в Lean. «Следовательно, мне либо придётся читать возможно-неправильный шлак, либо ждать, пока другие сделают то же самое, либо ждать, пока кто-нибудь их формализует, прежде чем я смогу с уверенностью сказать, что результаты вообще верны». Озабоченность Баззарда разделили многие другие исследователи, у которых, предположительно, были на этой неделе и другие дела.

Баззард был далеко не одинок в беспокойстве об ИИ-«шлаке» — жаргонном обозначении низкокачественного, часто ошибочного материала, сгенерированного ИИ, который всё чаще появляется в интернете и в реальном мире, включая академические статьи. Как и в других областях, математики рассказали The Verge, что за последние годы они наблюдали огромный рост такого материала, создаваемого с помощью инструментов вроде ChatGPT и Claude. Многое из него сбивает с толку, трудночитаемо и демонстрирует слабое понимание предмета; особенно оно убого, когда дело доходит до указания авторства других исследователей. Предыдущие математические работы OpenAI были широко раскритикованы экспертами за