Axiom Math добилась формальной верификации масштабного проекта Stacks для обеспечения безопасности математики с поддержкой ИИ

Image: TechCrunch · Source

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

Быстрый поток математических доказательств, созданных искусственным интеллектом, вызвал обеспокоенность по поводу надежности и точности таких работ. В последние месяцы модели ИИ подали сотни рукописей с претензией на решения сложных математических задач, однако даже традиционные компьютерные проверки порой не выявляли ошибок. Стремясь решить эту проблему, стартап Axiom Math, оцененный в 1,6 миллиарда долларов, сосредоточился на создании строго проверенных математических основ посредством формальной верификации, гарантируя, что системы ИИ надежно генерируют и используют корректную математику.

5 ноября 2026 года Axiom Math объявила о знаковом достижении: формальной верификации проекта Stacks, одного из крупнейших и самых уважаемых математических сборников. Проект Stacks, начатый в 2005 году математиком Колумбийского университета Йоханом де Йонгом, вырос в открытое совместное произведение, охватывающее широкий спектр тем от алгебры до геометрии и теории чисел, занимающее примерно 7654 страницы.

Агенты ИИ Axiom перевели весь проект Stacks примерно в 16 миллионов строк кода на Lean — формальном языке доказательств. Этот перевод позволил программному обеспечению для помощи в доказательствах тщательно проверить каждое доказательство, подтверждая логическую корректность во всем этом обширном и глубоко взаимосвязанном корпусе работ. Обеспечение целостности этих связей было значительной проблемой, которую генеральный директор Карина Хонг сравнила с согласованием хрупких структур в огромном целом без противоречий.

Компания была основана в марте 2025 года Хонг, бывшей аспиранткой по математике из Стэнфорда; ранее в этом году Axiom привлек 200 миллионов долларов в раунде серии А во главе с Menlo Ventures. Подход компании предусматривает предоставление агентам ИИ гибкой рамки для сотрудничества, позволяя параллельно работать над разными задачами при сохранении общей иерархической структуры, необходимой для поддержания зависимостей в проекте Stacks.

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

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

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

Генеральный директор Хонг подчеркивает, что будущее ИИ в исследованиях и инженерии зависит от доступных, многоразовых и тщательно построенных баз знаний, чтобы предотвратить распространение ошибок или «неряшливости». Она призывает другие компании, ориентированные на кодирование, попытаться провести формальную верификацию в аналогичных масштабах и ожидает, что совместно работающие асинхронно и стратегически агенты ИИ станут нормой в научных и программных достижениях.

Соединяя строгость человеческой математической точности с вычислительной мощью ИИ, работа Axiom Math над проектом Stacks знаменует важный шаг к надежной математике и созданию программного обеспечения с поддержкой ИИ, потенциально меняя то, как сложные области знаний формализуются и расширяются в ближайшие годы.