ИИ AxiomProver решил 9 из 12 сложных математических задач в Lean

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

Процесс разработки включал в себя формализацию задач командой разработчиков (внутренний хакатон «Prove-a-ton») и последующую работу AxiomProver в полностью автономном режиме. В течение 58 минут после старта, система решила 8 задач, а девятая – к полудню следующего дня.

Все доказательства, полученные AxiomProver, были проверены компилятором на 100% и реализованы в Lean 4 и Mathlib. Уровень сложности задач превосходит IMO, которым ранее хвастались Google и OpenAI.

Основательница стартапа, 24-летняя Карина Хонг, выпускница MIT с двумя дипломами математики и физики, привлекает к себе внимание благодаря своим академическим достижениям и опыту работы в Meta AI for Math.

В команду Axiom присоединился Кен Оно, эксперт в области теории чисел и эллиптических кривых, ранее занимавший должность вице-президента AMS и менторствующий выпускников Putnam Fellows.

На сегодняшний день у компании 17 сотрудников, в числе которых аспиранты и постдокторы из ведущих университетов, таких как MIT, Cambridge, Imperial и Humboldt. Axiom привлек $64 млн инвестиций от Menlo Ventures.