Axiom Math применила ИИ-агентов для верификации библиотеки Stacks Project

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

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

Использование формальных методов в математике традиционно требовало огромных временных затрат от ученых, так как написание кода для систем проверки доказательств (таких как Lean или Coq) является трудоемким процессом. Агенты стартапа автоматизируют этот этап, переводя естественный математический язык в машиночитаемый формат, пригодный для строгой проверки.

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