OpenAI сообщила, что её внутренняя ИИ-модель нашла опровержение гипотезы об экспоненциальном времени — ETH. На эту гипотезу опираются сотни работ по теоретической информатике.
ETH описывает сложность задачи выполнимости булевых формул. Проще говоря, речь идёт о поиске значений, при которых логическое выражение становится истинным. Гипотеза утверждает, что в общем случае такую задачу нельзя решить существенно быстрее полного перебора с экспоненциальным ростом времени.
Исследователи использовали ETH, чтобы доказывать сложность задач из теории графов, вычислительной биологии и баз данных. Она также тесно связана с вопросом о равенстве классов P и NP, но её опровержение само по себе этот вопрос не решает.
По данным OpenAI, модель получила результат 16 октября. На следующий день доказательство проверили в Lean — системе, которая формально проверяет каждый логический шаг. Компания опубликовала текст рассуждений модели и формализованное доказательство на GitHub.
Теперь работу независимо изучат Рассел Импальяццо и Рамамохан Патури из Калифорнийского университета в Сан-Диего, участвовавшие в создании ETH, а также Райан Уильямс, профессор MIT. Они подчеркнули, что их участие не означает подтверждения результата.
Учёные попросили OpenAI открыть все исходные данные и профинансировать конференцию для проверки доказательства. Компания согласилась. Исследователи не подписывали соглашений о неразглашении и не получают оплату за эту работу.
В тот же день OpenAI объявила ещё о двух результатах своих моделей: доказательстве гипотезы о локальном сглаживании в математике и доказательстве существования некоторых квантовых теорий поля в четырёх измерениях. Второй результат включает чистую теорию Янга — Миллса, связанную с одной из задач тысячелетия.
Пока ETH не считается опровергнутой: опубликовано заявление OpenAI и машинно проверенное доказательство, но независимая научная экспертиза ещё не завершена.
