ИИ-агенты научились формализовать учебники по вычислительной математике — новая методика оценки выявила скрытые проблемы
Группа исследователей представила работу, в которой кодирующий ИИ-агент применили для формализации учебника Numerical Methods for Ordinary Differential Equations в системе Lean 4. Ранее подобные проекты ограничивались разделами математики, уже хорошо описанными в библиотеке mathlib, тогда как вычислительная математика оставалась почти не охваченной.
Традиционно успех формализации измеряют только тем, проходит ли код проверку ядром (kernel acceptance). Авторы работы сочли такой подход недостаточным и предложили новую трёхмерную систему оценки: семантическая корректность, степень повторного использования функций mathlib и анализ с помощью LLM в качестве судьи (LLM-as-judge).
Применив эту методику к собственной формализации, а также к результатам двух других систем — RepoProver и M2F, — исследователи обнаружили повторяющиеся проблемы. Среди них: неполные многочастные утверждения, добавление ослабляющих гипотез и неоправданные ограничения на параметры, которые компилятор не замечает.
Таким образом, опора только на проверку ядром существенно завышает качество формализации. Авторы подчёркивают, что будущие системы автоматической формализации нуждаются в более строгих и воспроизводимых критериях оценки.
Работа опубликована в архиве препринтов arXiv и уже привлекла внимание сообщества формальной верификации. Разработанная методология оценки может стать стандартом для дальнейших исследований в этой области.
