Axiom Math верифицировала Stacks Project, чтобы остановить AI-slop

Агенты Axiom перевели примерно 7654 страницы в около 16 млн строк кода на языке Lean, который построчно проверяет программа-ассистент доказательств. Если доказательство проходит проверку, ему можно доверять как логически корректному. Сложность в том, что теоремы и определения в Stacks связаны между собой, и все связи нужно было сохранить. Сначала команда сомневалась в успехе. По словам CEO Карины Хун, большие и хрупкие вещи редко сочетаются.

Агенты работают параллельно

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

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

Почему это важно

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

Хун уверена, что агентам нужна переиспользуемая библиотека знаний, чтобы не плодить «слоп», и бросает вызов компаниям, пишущим код, — заняться формализацией в таком же масштабе. Axiom основана в марте 2025 года, а в марте этого года привлекла 200 млн долларов в раунде Series A под руководством Menlo Ventures.