Агент Axiom Prover решил 12 из 12 задач на самом сложном математическом экзамене в мире

Возможно, вы помните, что это за система. В начале декабря (когда и проводился конкурс Putnam, о котором идет речь) она решила 8 из 12 задач за отведенное на олимпиаду время + еще одну вне зачета. Это очень классный результат: большинство студентов получает круглый ноль.

Теперь разработчики сообщили, что агент дорешал самые сложные оставшиеся задачи и выложили все его решения сюда.

Интересно, что среди задач явно выделяются группы таких, которые(1) просты для человека и сложны для ИИ; (2) и наоборот. Например:

– Комбинаторные задачи человек решает достаточно быстро, а Axiom Prover одна из таких обошлась в 2054 строки формального кода и 518 минут вычислений. Это из-за того, что Lean, в котором работает агент, требует формального доказательства даже очевидных фактов, и они получались крупными и долгими, хотя человеку было бы достаточно одной фразы.

– Есть задачи, где у ИИ и человека кардинально разный подход. Например, A4: люди думали алгебраически, а Axiom Prover внезапно подошел геометрически. Это занятно.

– А вот А6 ни один штатный математик Axiom не смог решить, а Axiom Prover довольно быстро довел решение от идеи до формального доказательства.

Короче: все равно люди все еще выигрывают в плане математической интуиции. Для ИИ задача становится сложной, если нет готовых библиотечных кирпичей + идеи. Плюс, внезапным узким местом становится доказательство мелких фактов (опять же, для человека это вопрос интуиции).

axiommath.ai/territory/from-seeing-why-to-checking-everything