AxiomMath проверила Stacks Project: 16 млн строк кода Lean

Стартап AxiomMath объявил о формальной верификации Stacks Project — одного из крупнейших созданных людьми корпусов математических текстов. ИИ-агенты компании перевели примерно 7 654 страницы библиотеки в около 16 млн строк кода на Lean, который проверяется программой-помощником доказательств.

Что проверила AxiomMath

Stacks Project был запущен в 2005 году математиком Колумбийского университета Йоханом де Йонгом как открытый справочник. Над ним продолжают работать математики: библиотека охватывает материал от университетской алгебры до продвинутых тем алгебры, геометрии и теории чисел.

Формализация не сводится к переносу текста в другой формат. Доказательство записывается в виде программы на Lean, а proof assistant последовательно проверяет его. Успешная проверка означает, что доказательство логически корректно в рамках использованной формальной системы.

Для Stacks задача осложнялась связями между определениями и теоремами. Многие результаты опираются на предыдущие, поэтому команде требовалось сохранить зависимости во всём массиве из 16 млн строк кода. Генеральный директор Axiom Карина Хонг отметила, что определения не должны противоречить друг другу, а теоремы должны оставаться согласованными.

Как работали агенты

По словам сотрудника технической команды Axiom Ашвина Сваминатана, компания задала агентам иерархию, но не расписывала каждое действие. Агенты самостоятельно находили задачи, которые можно выполнять параллельно. Axiom также обучала собственные модели для математических задач; на раннем этапе эксперт компании по Lean помогал направлять их работу.

В Axiom считают, что формализация закрывает заметный пробел для алгебраической геометрии. Ранее исследователям, желавшим проверять новые работы в этой области через Lean, было мало на что опереться. Теперь проверенный корпус Stacks может служить базой для последующих доказательств.

Почему это важно для разработки

Формальная верификация применяется не только в математике: инженеры используют её при проверке проектов микросхем, а исследователи во Франции применяли подход для поиска ошибок в ПО, рассчитывающем семейные пособия. Axiom намерена использовать полученный опыт и в создании программного обеспечения.

Компания связывает эту задачу с ростом числа ИИ-агентов, которые пишут код. Её подход состоит в том, чтобы агенты строили новые результаты на повторно используемой и проверенной базе, а не начинали работу без надёжной основы. Для бизнеса практический вывод прост: при внедрении генеративных инструментов в критичные процессы особенно важны проверяемые зависимости, формальные ограничения и контроль корректности, а не только скорость генерации кода.