AxiomMath делает ставку на то, что математика сможет избежать этой участи не за счет замедления, а за счет более прочного фундамента. Стартап стоимостью 1,6 миллиарда долларов стремится создать верифицированную основу, на которую ИИ-агенты смогут опираться при написании программного обеспечения и, в конечном итоге, при проведении научных исследований.
В среду компания объявила о формальной верификации Stacks Project — одного из крупнейших собраний математических трудов, когда-либо написанных человеком. Математики часто высоко оценивают Stacks: математик из Колумбийского университета Питер Войт утверждал, что «ничто другое не сравнится», сравнивая проект с «знаменитыми книгами Бурбаки» — серией, которая «перестроила математику с нуля» в XX веке.
Коллега Войта по Колумбийскому университету Йохан де Йонг основал Stacks Project в 2005 году как открытый справочник. С тех пор математики вносили в него свой вклад, развивая результаты от алгебры университетского уровня до самых передовых идей в области алгебры, геометрии и теории чисел.
Парк ИИ-агентов компании переводит примерно 7654 страницы библиотеки в около 16 миллионов строк кода, проверенного компьютером.
Формализация математики — это способ убедиться в надежности лежащей в ее основе структуры. Математики переписывают доказательства в виде кода на языке программирования Lean, а программа-ассистент проверяет код построчно. Если доказательство проходит проверку, математики могут быть уверены в его логической непротиворечивости.
Инженеры используют ту же идею, называемую формальной верификацией, чтобы подтвердить работоспособность своих разработок микросхем, а исследователи во Франции использовали ее для обнаружения ошибок в программном обеспечении, рассчитывающем семейные пособия.
Для такой библиотеки, как Stacks Project, проверка каждой теоремы — лишь часть работы. Теоремы и определения в Stacks взаимосвязаны, и каждое из них опирается на предыдущие. Подобно генеалогическому древу, многие результаты в Stacks восходят к тем, что были получены ранее.
Эта взаимосвязанность поначалу вызывала у Axiom сомнения в успехе проекта. Команде пришлось сохранить каждую связь в целости в объеме около 16 миллионов строк кода на Lean.
«Большие и хрупкие вещи в жизни плохо сочетаются», — сказала генеральный директор Axiom Карина Хонг в интервью TechCrunch. «[Stacks] — это собрание математических результатов, которое является фундаментом математики. Вы хотите, чтобы [теоремы] были последовательными, а не парадоксальными. Вы хотите, чтобы определения не противоречили друг другу».
25-летний генеральный директор бросила аспирантуру по математике в Стэнфорде и основала компанию в марте 2025 года. В марте Axiom привлекла 200 миллионов долларов в рамках раунда Серии А под руководством Menlo Ventures.
«Мы не были уверены, сможет ли «вибрационный» код сохранить красоту Stacks», — сказала Хонг.
Чтобы осуществить проект, команда предоставила своим агентам свободную структуру и позволила им работать параллельно. «Со Stacks мы ввели иерархию… [но] это не была полная иерархия, диктующая, что делает каждый агент», — сказал Ашвин Сваминатан, сотрудник технического отдела Axiom. «Агенты сами находили задачи и определяли, над чем они могли бы работать параллельно».
Axiom также обучила собственные модели для работы с математикой — подход, который, по словам Хонг, большинство других стартапов в области верификации не использовали. Сначала команда полагалась на одного из своих внутренних экспертов по Lean, чтобы привить агентам человеческое чувство вкуса. Со временем, по словам Хонг, агенты приобрели этот вкус самостоятельно.
Результат заполняет один из самых больших пробелов в формализованной математике. «Когда вы смотрите на то, что было формализовано в математике, существует эта огромная черная дыра. И эта черная дыра охватывает алгебраическую геометрию», — сказал Сваминатан.
До сих пор у исследователей, желавших проверить новые работы по алгебраической геометрии с помощью Lean, было мало наработок, сказал Сваминатан. «Ну, теперь они есть».
Axiom утверждает, что каждый верифицированный результат становится строительным блоком, поэтому будущие доказательства могут опираться на проверенную математику, а не начинать с нуля. Теренс Тао, математик из Калифорнийского университета в Лос-Анджелесе и обладатель Филдсовской премии, более просто сформулировал общую идею: «Чем больше у вас формализованных доказательств, тем больше формализованных доказательств вы можете создать».
Математики — не единственная целевая аудитория Axiom. Разработчики давно борются за гарантию того, что их код не содержит ошибок и уязвимостей. Эта проблема усугубляется по мере того, как ИИ-агенты пишут все больше кода в мире.
Axiom делает ставку на то, что программное обеспечение будущего будет нуждаться в опоре на верифицированные основы, подобно тому, как это теперь делает Stacks.
«Мы считаем, что математика — это область, с которой начинается создание этих вещей, и что это передаваемый навык», — сказал Сваминатан. «Агенты могут читать наш код, понимать его и создавать на его основе новую инфраструктуру. Наша формализация на Lean теперь является субстратом, на котором агенты могут строить».
То, как агенты Axiom создавали Stacks, работая параллельно и выбирая собственные задачи, — это то, как, по мнению Хонг, будет происходить большая часть будущей работы ИИ. ИИ-агентам, утверждает она, потребуется хорошо построенный, многоразовый массив знаний, чтобы не производить «шлак».
«Вы хотите, чтобы [агенты] имели многоразовую библиотеку для построения и продвижения вперед», — сказала Хонг. «Если вы изначально допускаете ошибки из-за плохих инженерных решений, им будет очень трудно расширить эти границы».
Хонг настолько уверена в этом подходе, что бросает вызов: «Я открыто призываю все компании, занимающиеся разработкой кода, работать над формализацией в таком масштабе».
Всегда имейте в виду, что редакции могут придерживаться предвзятых взглядов в освещении новостей.
Автор – Aditya Mehta
