OpenAI 1 августа сообщила, что внутренняя версия её следующей флагманской модели — Astra — получила новые результаты по десяти открытым задачам математики и теоретической информатики.
Общий критерий отбора: по главным выводам этих задач не было прогресса минимум десять лет.
Отличие от прошлых заявлений в духе «ИИ решил математику» — в проверяемости. Доказательства формализованы в Lean 4: это язык, где теорему записывают строгими символами, а компьютер сам проверяет каждый шаг рассуждения на соответствие правилам. Верить OpenAI на слово не нужно. Данные лежат на GitHub в репозитории openai/ten-proofs, сама статья занимает 249 страниц.
Верхняя граница плотности упаковки шаров в больших размерностях подтянута к теоретическому пределу метода Кона—Элкиса — общий показатель для высоких размерностей не улучшался с 1978 года. Для двоичных и сферических кодов границы улучшены впервые с 1977 и 1978 годов, причём экспоненциально.
Ещё в списке: построена группа-контрпример к гипотезе жёсткости Конна, доказана теорема о параллельном повторении для любых конечных игр двух игроков с квантовой запутанностью, доказана гипотеза Эрхарта об объёме во всех размерностях, получены контрпримеры к двум гипотезам экстремальной теории графов и новые нижние оценки сложности для вычисления перманента матрицы.
Аргументы придумывала Astra. Люди оформляли их в текст статьи, после чего Astra формализовала доказательства в Lean. Ответственность за корректность OpenAI берёт на себя.
Все токены, потраченные на поиск решений, по прайсу Sol API от OpenAI обошлись бы примерно в $2000.
Отдельно выложен PDF с разбором хода мысли — но это не сырые логи. Другая модель прочитала записи рассуждений и готовые статьи и восстановила путь к доказательству: тупиковые направления, смены подхода, финальную идею.
Саму Astra ещё не выпустили. Доказательства опубликовали раньше модели.
