В данной статье представлена матрица покрытия сигналов для стратификации ошибок типа и семантических ошибок в процессе автоматической формализации LLM, что позволяет выйти за рамки скалярных метрик корректности типа. Фреймворк классифицирует выходные данные на ячейки истинного успеха, только ошибка типа, только ошибка семантики или оба вида неудач, пересекая результаты элаборатора Lean с оценками семантической эквивалентности.

  • Анализ ProofNet# и MiniF2F-test с использованием DeepSeek V4-Pro показывает, что методы elab-feedback восстанавливают примерно 64% ошибок страты типа, увеличивая долю истинного успеха на 34–36 процентных пунктов.
  • Коэффициент восстановления из «только ошибка типа» в «истинный успех» предсказывает дельту истинного успеха на отложенных методах с точностью 2/186 и демонстрирует линейную зависимость дельты корректности типа от доли неудач базового элаборатора с коэффициентом детерминации R-squared = 0.96.
  • Символические судьи расходятся с семантическими судьями на 26–37 процентных пунктов в оценке выходов elab-feedback, причем ложноотрицательные результаты часто обусловлены переписываниями, навязанными элаборатором.

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