Агент 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