Опровержение гипотезы экспоненциального времени
• Модели OpenAI и Anthropic независимо опровергли гипотезу экспоненциального времени. • Гипотеза предполагает экспоненциальный рост времени решения задач с увеличением размера входных данных.
Задача 3-SAT
• Задача 3-SAT требует определить, можно ли присвоить значения переменным булевой формулы, чтобы она стала истинной. • Формула состоит из условий с тремя переменными или их отрицаниями. • Гипотеза утверждает, что задачу нельзя решить быстрее, чем за экспоненциальное время.
Доказательства и их проверка
• Обе компании опубликовали опровержения на языке Lean. • Доказательство OpenAI позволяет предсказать число решений булевых формул за субэкспоненциальное время. • Результаты предстоит проверить независимым специалистам, включая авторов гипотезы Рассела Импальяццо и Рамамохана Патури.
Последствия опровержения
• Гипотеза используется для обоснования сложности задач в теории графов, вычислительной биологии и геометрии. • Подтверждение опровержения потребует пересмотра результатов, основанных на этой гипотезе. • Практические последствия неясны, так как быстрый алгоритм в теории не всегда эффективен на реальных задачах.
Предыдущие достижения OpenAI
• Внутренняя модель OpenAI ранее решила 372 задачи из разных областей математики. • Модель пока не вышла в открытый доступ.