OpenAI заявила, что её новейшая модель ИИ решила 10 мировых проблем, включая опровержение гипотезы жёсткости Конна.
На следующий день появилась статья-ответ от человека: контрпример, предложенный ИИ, несостоятелен.
Автор — Дж. Л. Нильсен из Центра топологической физики Канзасского университета. Он проследил с начала до конца 37 000 строк кода на Lean 4, опубликованного OpenAI, сопоставил каждый объект с его математическим прототипом и в итоге указал на два независимых пути неудачи.
Конкретный процесс доказательства нам, обычным людям, не совсем понятен, пусть ИИ и математики сражаются на своём уровне.
Но этот случай показывает, что проверка результатов научных исследований ИИ людьми по-прежнему критически важна.
Что такое гипотеза жёсткости Конна
Гипотеза жёсткости Конна говорит о следующем.
Математически можно сопоставить группе алгебраическую структуру. Иногда две разные на вид группы порождают совершенно одинаковые структуры.
Конн около 1980 года выдвинул предположение: при условии, что группа удовлетворяет двум дополнительным условиям, такая ситуация невозможна — если структуры одинаковы, то и группы должны быть одинаковыми.
Эти два дополнительных условия — одно называется ICC, другое — свойство (T) Каждана.
Другими словами, чтобы опровергнуть эту гипотезу, нужно привести пример двух групп, удовлетворяющих обоим условиям, но имеющих разное строение.
Новая модель OpenAI поступила так: сконструировала две неизоморфные группы, которые порождают одинаковые алгебры, и представила доказательство того, что обе группы удовлетворяют ICC и свойству (T).
Весь аргумент был записан в виде 37 000 строк кода на Lean 4, проверенных ядром Lean строка за строкой, с приложением пояснительного документа о том, как были построены эти группы.
Нильсен указывает: одна из групп, сконструированных ИИ, на самом деле не удовлетворяет дополнительным условиям — ни ICC, ни свойству (T).
Есть три возможных причины:
свойство (T) в коде не точно соответствует исходному определению Каждана; или доказательство верно лишь частично, но было распространено на всю группу; либо группа в коде вообще не соответствует описанию в пояснительном документе.
37 000 строк, построчное сопоставление
Чтобы проверить этот вывод, Нильсен проделал ещё более трудоёмкую работу.
Опубликованный код представляет собой единый файл, имена из исходных модулей на ранних этапах в нём отсутствуют.
Он составил таблицу соответствий, указав для каждого математического объекта его имя и номер строки в новом коде:
группа коцепей над нулём находится на строке 13700, скрученная группа — на строке 14069, доказательство изоморфизма двух алгебр — на строке 36712, основная теорема — на строке 36954.
Он также проследил всю цепочку рассуждений, доказывающую ICC в коде. Эта цепочка начинается со строки 31430, передаётся слой за слоем и, наконец, формирует заключение на строке 31610.
Проблема, указанная Нильсеном, заключается в том, что эти леммы имеют дело с объектами, полученными после дуализирующего преобразования, а не с исходной группой, содержащей центральный элемент, и поэтому они напрямую не охватывают ключевые элементы.
Вопрос о том, выполняются ли они для каждого элемента конкретной группы, которая в итоге попадает в теорему, зависит от того, как соединяются две части конструкции.
Это показывает, что проблема в «том, что нужно доказать», а не в «правильности доказательства». Lean отвечает только за проверку последнего.
Относительно другой скрученной группы Нильсен настроен сдержанно. Он говорит, что не проверял независимо по коду, удовлетворяет ли она ICC, и признаёт, что леммы в коде, возможно, действительно доказывают это, но это не меняет вывода: одно из условий уже не выполнено.
Он также записал свои два контраргумента в виде кода на Lean, который компилируется в Lean 4.32.2.
Машина проверяет форму, а не смысл
В последнем разделе статьи это событие помещается в более широкий контекст.
Ядро Lean гарантирует лишь то, что доказательство формально безупречно, но не отвечает за то, действительно ли оно доказывает исходное утверждение.
Здесь можно прямо процитировать Теренса Тао: проверяющее доказательство — это само формальное утверждение, а не его соответствие намерению, поэтому проверку человеком нельзя полностью заменить.
Подобные инциденты уже случались ранее.
Аудит пяти часто используемых наборов тестов для Lean выявил 4833 случая, включая контрпримеры, пустые теоремы и ненадёжные аксиомы, которые все прошли машинную проверку. В итоге люди сконструировали контрпримеры и обнаружили, что само доказываемое утверждение было неверным.
В работе по формализации статистической теории обучения наиболее опасная ситуация описывается как «не неудачное доказательство, а успешное доказательство неверного утверждения».
Исследования в области тензорных сетей также фиксировали аналогичные явления: система выдавала доказательство, формально совершенно правильное, но доказывающее утверждение более слабое, чем ожидалось.
Нильсен пишет, что, возможно, формализация OpenAI правильно установила каждое из своих заявленных заключений. Но то, что она не установила и что ядро Lean не может проверить, — это связь этих заключений с исходной формулировкой гипотезы.
Человек, читая гипотезу, видит предпосылки. Помощник в доказательствах, получив заключение, которое не удовлетворяет предпосылкам, всё равно проверит любое утверждение о нём.
Гипотеза жёсткости Конна по-прежнему остаётся открытой.
Адрес статьи:
https://philarchive.org/archive/NIEWTCv17
Ссылки:
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
Статья из WeChat-аккаунта «Квантовый бит», автор: Мэн Чэнь
