Axiom Math использует ИИ для верификации математических доказательств

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

• В рамках проекта 7654 страницы математических текстов были переведены в 16 миллионов строк кода на языке Lean.
• ИИ-агенты Axiom работали параллельно, самостоятельно распределяя задачи и проверяя логическую связность доказательств.
• Верифицированные результаты теперь служат надежной базой для дальнейших исследований в области алгебраической геометрии.
• Основательница компании Карина Хонг бросила вызов другим технологическим компаниям, призвав их к масштабной формализации знаний.

Новое слово в математической точности Формальная верификация — это процесс, при котором доказательства переписываются как программный код, а специальный инструмент (пров-ассистент) проверяет каждое утверждение строка за строкой. Stacks Project, запущенный Йоханом де Йонгом в 2005 году, охватывает широкий спектр дисциплин, от алгебры до теории чисел. До недавнего времени его сложность была «черной дырой» в формализованной математике, так как все теоремы в нем тесно взаимосвязаны.

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

Значение для индустрии и программирования Для разработчиков и бизнеса это означает переход к «верифицируемой разработке». Поскольку ИИ-агенты пишут все больше программного кода, критически важно, чтобы их база знаний была свободна от ошибок. Axiom утверждает, что проверенная математика станет фундаментом, на котором агенты смогут строить надежную инфраструктуру, избегая генерации некачественного кода (slop).