OpenAI опубликовала 249-страничный отчет о внутренней модели Astra, которая якобы достигла 10 новых результатов в математике, включая построение первой не-софической группы и опровержение гипотезы Конна.
Компания OpenAI анонсировала исследовательскую работу, посвященную внутренней модели Astra. По заявлению разработчиков, система смогла самостоятельно найти ключевые идеи для решения десяти давно открытых математических задач, а затем формализовать доказательства в системе Lean, получив машинно проверяемые сертификаты корректности. Общий объем публикации составляет 249 страниц, а вычислительные затраты оцениваются примерно в $2000 по текущим тарифам Sol API.
Среди заявленных достижений — построение первого явного примера не-софической группы, существование которой обсуждалось десятилетиями, опровержение гипотезы жёсткости Конна из теории операторных алгебр, доказательство квантовой теоремы о параллельном повторении для общих двухигровых систем и доказательство гипотезы Эрхарта об объёме. Также сообщается о первом за 44 года улучшении общей верхней оценки плотности упаковки сфер — задачи, связанной с теорией кодирования и криптографией.
Особенность Astra заключается в режиме работы исследовательской системы, а не обычного чат-бота: модель анализирует открытую задачу, генерирует математические идеи, строит доказательство, переводит его на язык Lean и проходит машинную верификацию. Использование Lean — системы формальной верификации — позволяет исключить логические ошибки, однако научное сообщество всё равно должен проверить корректность постановок задач, новизну результатов и их соответствие литературе. История знает случаи, когда громкие заявления требовали месяцев независимой экспертизы.
