Lean-компиляция завышает точность формализации: разрыв до 29,5 п.п.

Lean принимает объявление, если оно корректно типизировано. Что оно говорит по смыслу, компилятор не проверяет. Авторы работы «Beyond Compilation» измерили, насколько метрика «скомпилировалось» завышает качество автоформализации, то есть перевода математических утверждений с естественного языка в Lean. Самая яркая цифра: агент с инструментами компилирует 87,2% из 227 университетских утверждений, но семантический критерий пропускает только 57,7%. Разница в 29,5 процентного пункта — это Lean-код, который выглядит безупречно и формулирует не то, что просили.

Как устроена проверка

У большинства задач нет эталонного Lean-перевода, поэтому сравнивать с «золотым» ответом нельзя. Авторы вводят составной критерий: утверждение принимается, если оно компилируется в Lean и две LLM-модели из разных семейств независимо признают его верным переводом исходной формулировки.

Критерий проверили на независимом случайном аудите. С мнением большинства людей-разметчиков он совпал в 91,5% случаев. Ошибается он несимметрично: неверный перевод пропускает редко, а часть верных отклоняет. То есть оценка консервативная и скорее занижает результат систем.

Основные результаты по восьми системам:

• разрыв между долей скомпилированных и принятых утверждений — от 1,3 до 29,5 п.п.;
• агент с инструментами: 87,2% компиляции против 57,7% принятых;
• люди просмотрели все отказы агента: 23,8 из 29,5 п.п. оказались реальными ошибками перевода;
• у шести из семи систем с одним проходом (one-shot) 78–100% разрыва — настоящие ошибки перевода, по двухэтапному ревью Claude Opus 5.5 с Lean и GPT-6.1 Sol, сверенному с человеческой разметкой.

Когда ошибается судья

Самая неожиданная часть — про новые модели. GPT-5.2 был одним из двух судей. Авторы дали ему оценить переводы двух более поздних моделей, GPT-6 Astra и Claude Opus 5.5. Судья принял по 83% утверждений у каждой. Собственный one-shot-результат GPT-5.2 при этом — 21%.

Дальше двухэтапное ревью разобрало отказы этих двух моделей. Из 54 отклонённых утверждений реальными ошибками перевода оказались только 4, то есть 7%. Остальные отказы — промахи судьи. Это согласуется с простой логикой: чем реже система ошибается, тем меньше среди её отказов настоящих ошибок и тем заметнее становится шум самого судьи. Судья, который не растёт вместе с оцениваемыми моделями, становится узким местом бенчмарка.

Для индустрии вывод неприятный. Метрика на основе LLM-судьи у слабых систем почти честна, а у сильных начинает занижать качество. Сравнивать по ней модели разных поколений без повторной проверки отказов нельзя.

Что показала абляция инструментов

Авторы прогнали агента через абляцию 2^3, то есть включали и выключали три инструмента во всех восьми комбинациях. Основной прирост компиляции даёт обратная связь от Lean: агент видит ошибки и правит код. Но почти половина этого прироста семантический критерий не проходит. Агент учится добиваться компиляции, а не точности смысла. Типичный эффект: чтобы убрать ошибку, из утверждения выпадает условие, ослабляется квантор или подменяется структура.

Что менять в практике

Если вы строите пайплайн автоформализации или обучаете модель на сигнале от Lean, компиляция как единственная награда даёт смещённую оценку и подталкивает к вырожденным формулировкам. Нужен хотя бы один семантический слой: судьи из разных семейств и выборочная человеческая проверка отказов.

При работе с новыми моделями стоит проверять, не отстаёт ли судья от оцениваемой системы. Если большая часть отказов оказывается ошибками судьи, а не перевода, метрику пора пересматривать. Код и данные опубликованы на GitHub (grenadeComing/beyond-compilation), так что подход можно воспроизвести на собственных утверждениях.