OpenAI раскрыла промпт к заявленному опровержению ETH

OpenAI поделилась промптом, после которого её внутренние модели, по словам компании, опровергли гипотезу об экспоненциальном времени (ETH). В нём модель просят найти детерминированный алгоритм для k-SAT (проверки выполнимости логической формулы, где в каждом условии не больше k переменных или их отрицаний) со временем 2^((1-ε)n) с точностью до полиномиального множителя, причём одна и та же ε больше нуля должна работать для любого k от 3 и выше. Текст, который 13 ноября опубликовал блог Ethdiscussion, показывает постановку задачи, но не доказательство: опровержение по-прежнему остаётся заявлением OpenAI, и разбирать его взялись Рассел Импальяццо, Рамамохан Патури и Райан Уильямс.

Формально промпт целится в SETH, сильную версию гипотезы, причём в детерминированном варианте. ETH, которую Импальяццо и Патури из Калифорнийского университета в Сан-Диего предложили в конце 1990-х, утверждает, что существует δ > 0, при котором 3-SAT нельзя решить за O(2^(δn)). SETH идёт дальше: в определении из работы Импальяццо и Патури 2013 года, на которую ссылается промпт, лучший показатель экспоненты для k-SAT с ростом k стремится к 1, к полному перебору. Модель просят доказать, что этот предел меньше 1. Рукопись, которую OpenAI выложила в репозиторий openai/math, при этом называется «The Exponential Time Hypothesis is False».

Алгоритм, константа и степень полинома могут зависеть от k, ε - нет. Каждый алгоритм должен быть конечным, верным для входа любой длины и обходиться без подсказок, зависящих от этой длины. В оценку времени модель обязана включить чтение входа, предобработку, ветвление, вспомогательные построения, вызовы подпрограмм и дерандомизацию, перевод вероятностного алгоритма в детерминированный. Для заявленного алгоритма нужно доказать остановку и корректность и на выполнимых, и на невыполнимых формулах, а для ε показать доказанную нижнюю границу, не зависящую от k.

Промпт дотошно перечисляет, что опровержением не считается: улучшения лишь для конечного числа значений k, экономия ε_k, которая уходит к нулю с ростом k, алгоритмы для среднего случая или для входов с заранее обещанными свойствами, шаги через неподтверждённый оракул и рандомизированные алгоритмы без корректного перевода в детерминированные. Условный результат запрещено называть безусловным опровержением. Вторая ссылка в промпте, на работу Цыгана (Cygan) и соавторов «On Problems as Hard as CNF-SAT», идёт с оговоркой: там используются рандомизированные алгоритмы с ограниченной ошибкой, и эту договорённость модель должна держать отдельно от детерминированной цели.

Модель также просят не исходить из того, что опровержение существует, и не выдавать неполный аргумент за доказательство. Если цель не достигнута, она должна прямо сказать, что опровержения нет, отделить доказанные леммы от гипотез и неудачных подходов и назвать точное математическое препятствие, которое осталось. «Полезный строгий частичный прогресс предпочтительнее выдуманного решения», - сказано в промпте.

Рабочая группа специалистов по информатике, как сообщал TechCrunch, просила OpenAI выложить доказательства публично и оплатить конференцию. Уильямс в октябре назвал выгрузку доказательств OpenAI «DDoS-атакой на математиков», но согласился помочь в их интерпретации вместе с Импальяццо и Патури; первым шагом стало открытое письмо с призывом к обсуждению и выработке норм для вкладов ИИ. Математик Anthropic Левент Альпёге тогда же предположил, что OpenAI строила свои решения на уже существующих работах, а через несколько часов Anthropic выпустила собственное опровержение ETH.

Сам аргумент модель OpenAI нашла 16 октября, а на следующий день его проверили в Lean, системе машинной проверки доказательств. Промпт, который к нему привёл, компания согласилась выложить в открытый доступ.