ИИ справился с формализацией теоремы, но провалил экспертизу: новое исследование
Исследователи изучили, насколько полуавтономная формализация математических теорем с помощью больших языковых моделей (LLM) соответствует требованиям к библиотечному коду. В качестве примера они использовали теорему Гротендика об обращении в нуль — важный результат алгебраической геометрии.
Первоначальная версия формализации, созданная с участием LLM, компилировалась без единой ошибки (sorries — незакрытых пробелов в доказательстве). Однако экспертная проверка выявила серьёзные проблемы: некорректные определения, недостаточную общность теоремы, плохую организацию файлов и неудобный интерфейс программирования (API).
После этого команда провела процесс рефакторинга и сжатия кода на основе замечаний эксперта и получила вторую рецензию. Сравнение показало контраст: ИИ хорошо справлялся с локальными, механически проверяемыми исправлениями, но оставался слаб в выборе определений и проектировании API.
Авторы работы, опубликованной на arXiv, подчёркивают, что автоформализацию следует оценивать не только по отсутствию ошибок компиляции, но и по тому, выдерживает ли такая формализация экспертизу. Это важный шаг к пониманию реальных возможностей LLM в математическом доказательстве.
Исследование проводилось на базе интерактивного доказателя теорем Lean. Учёные надеются, что их подход поможет сделать автоматическую формализацию более практичной для использования в библиотеках формальной математики.
