GPT-5.6 за допомогою промпта закрив 30-річну прогалину в опуклій оптимізації

Допис на форумі r/math повідомляє, що GPT-5.6 Sol Pro за одну сесію тривалістю 148 хвилин видав другу половину результату про складність в опуклій оптимізації, який залишався відкритим із 1996 року. Автор супровідного препринту каже, що аргумент формально перевірено в Lean, і що результат ще не пройшов рецензування.

Що саме було відкритим

Йдеться про детерміновану опуклу оптимізацію нульового порядку. Алгоритм може запитати будь-яку точку одиничної кулі в R^d і отримує лише точне значення опуклої 1-ліпшицевої функції — без градієнтів — не маючи жодних інших обмежень ні на обчислення, ні на пам'ять. Такі задачі, де доступне лише значення функції, виникають, коли цільову функцію оцінюють фізичним експериментом або симулятором, і природне питання полягає в тому, скільки звернень принципово потрібно. У 1996 році Протасов запропонував алгоритм, який показує, що достатньо близько d² звернень. Відповідної нижньої оцінки бракувало: найсильніший придатний на той час результат, Ω(d), успадковувався від сильнішої моделі першого порядку, де градієнти доступні, і це залишало лінійну прогалину за d та не давало певності, що градієнти взагалі допомагають. Доведення, яке видав модель, закриває цю прогалину: жоден алгоритм не може бути кращим за порядок d² звернень, тож метод Протасова оптимальний.

Десятисторінковий промпт і 148 хвилин

Автор, викладач промислової інженерії та дослідження операцій у Каліфорнійському університеті в Берклі, працював над цією задачею уривками близько року і безуспішно пробував GPT-5.4 та GPT-5.5. Після того як OpenAI оголосила про своє доведення гіпотези про подвійне покриття циклами, він написав промпт обсягом приблизно десять сторінок у тому ж стилі — він доданий у кінці препринту — і попросив квадратичну нижню оцінку з точністю порядку d⁻⁴. Після 148 хвилин безперервної роботи модель повернув доведення, яке встановлює квадратичну залежність від розмірності з точністю порядку d⁻³. Автор перевірив аргумент самостійно й формально довів його в Lean. Конструкція — максимум афінних функцій — тісно пов'язана з тією, що стоїть за точною оцінкою Немировського та Юдіна для опуклої оптимізації першого порядку.

Що це означає для досліджень

Препринт, репозиторій Lean, повний промпт і оригінальні журнали чатів доступні за посиланнями з допису. Автор обережний в оцінці масштабу твердження: доведення не вносить принципово нових технік в опуклу геометрію, і, на його думку, якщо результат досяжний наявними методами, сучасні системи ШІ теж його досягнуть. Він не вважає, що математики стануть непотрібними, але каже, що працювати над легкими й навіть помірно складними задачами втратить сенс, а дослідникам залишаться ті, де справді потрібні нові ідеї. Коментатори розповідають про порівнянні результати тієї ж моделі, зокрема про доведення гіпотези сумісності Сабідуссі та одну відкриту задачу в кодах, що виправляють помилки, — обидва опубліковані на arXiv із формалізаціями в Lean. На питання про витрати автор оцінює проєкт у суму від 20 до 200 доларів підписки, а загальний час використання моделі — не більш ніж близько п'ятнадцяти годин.