ИИ не справляется с распознаванием теорем при изменении их формы: представлен тест TREAT
Исследователи представили новый бенчмарк TREAT, предназначенный для оценки того, насколько хорошо большие языковые модели распознают известные математические теоремы, когда их формулировка изменена эквивалентным преобразованием. Работа опубликована в виде препринта на arXiv.
Проблема, которую решают авторы, связана с тем, что ИИ-системы всё чаще работают одновременно с гибкими входными представлениями и формальными объектами, используемыми инструментами. Ключевой вызов — умение определить, что незнакомая формулировка обозначает уже известный формальный объект.
В отличие от простого пересказа текста теоремы, TREAT меняет саму математическую форму условий. Теоремы представлены через остаточные уравнения, утверждения о свидетелях, оптимизационные тождества, отношения множеств, операторные формы и промежуточные характеристики доказательств.
Для создания бенчмарка авторы собрали страницы с теоремами, отобрали записи с пригодными математическими выражениями, извлекли канонические условия и сгенерировали преобразованные варианты с записанными предположениями и обратными отображениями. Итоговый корпус включает 737 теорем и 29 480 преобразованных строк.
Результаты тестирования показали, что лучшая модель правильно определяет теорему лишь в 60,73% случаев. Другие системы демонстрируют разные типы ошибок: отказ от ответа, неверное распознавание и некорректный вывод.
По мнению авторов, это свидетельствует о хрупкости знаний ИИ о теоремах при эквивалентных изменениях представления. TREAT предлагает контролируемую среду для оценки устойчивости доступа к формальным знаниям, что важно для областей, требующих стабильных целевых объектов, явных отношений эквивалентности, процедур проверки и аудируемых результатов.
