ИИ OpenAI получил десять новых результатов в математике

Большие языковые модели обычно применяют для объяснения известных формул или проверки готовых вычислений. Новая работа OpenAI относится к другой категории: модель искала оригинальные математические аргументы для задач, которые ранее оставались нерешёнными.

Результаты охватывают сразу несколько областей:

• геометрию высоких размерностей;
• теорию кодирования;
• теорию групп;
• сложность арифметических схем;
• квантовую теорию сложности;
• решёточную криптографию;
• операторные алгебры;
• экстремальную комбинаторику.

OpenAI сообщает, что внутренняя версия следующей крупной модели Astra решила или существенно продвинула десять задач.

Среди опубликованных результатов – построение не-софической группы, опровержение гипотезы жёсткости Конна, новые оценки плотности упаковки сфер, усиленные границы для двоичных кодов и доказательство результатов для многокрасочных чисел Рамсея.

Отдельная работа посвящена задаче ближайшего вектора в решётке. Эта область имеет прямое отношение к сложности алгоритмов и постквантовой криптографии.

Модель не только сформировала математические аргументы. После подготовки рукописей каждый результат был формализован в Lean – системе, которая позволяет записывать доказательства в виде последовательности шагов, проверяемых компьютером.

Формализация не заменяет оценку математического значения результата научным сообществом, но помогает обнаруживать пропущенные условия, некорректные переходы и логические противоречия.

Компания также опубликовала рукописи, сертификаты Lean и отдельные разборы рассуждений модели.

Работа показывает потенциальный переход от ИИ как справочного инструмента к ИИ как участнику исследовательского процесса. При этом окончательная ценность результатов будет зависеть от их проверки, развития и использования профессиональными математиками.