Проблема «хрупких» знаний
Искусственный интеллект всё чаще используется для работы с формальными объектами, но возникает критическая проблема: модели не могут опознать знакомый результат, если он представлен в непривычной форме. Исследователи Fateme Mazdarani и Carlos Toxtli из Университета Ватерлоо представили бенчмарк TREAT (Theorem Recognition via Equivalent Algebraic Transformations), который проверяет способность LLM распознавать теоремы через эквивалентные математические преобразования, а не просто по тексту.
Как устроен тест
В отличие от стандартных датасетов, где теоремы перефразируются текстово, TREAT меняет саму математическую форму записи. Исследователи взяли 737 канонических теорем и создали 29 480 вариантов их записи, используя:
- Уравнения остатков (residual equations);
- Утверждения о свидетелях (witness statements);
- Оптимизационные тождества;
- Связи множеств и операторные формы.
Задача модели — по изменённому условию восстановить имя оригинальной теоремы.
Результаты: провал лидеров
Эксперименты показали, что даже самые продвинутые модели теряют формальные знания при смене нотации. Лучший на момент теста модель-кандидат достиг точности всего 60.73%. Остальные системы демонстрировали различные виды сбоев: от полного отказа от ответа (abstention) до генерации некорректных математических выражений.
| Метрика / Характеристика | Значение |
|---|---|
| Количество уникальных теорем | 737 |
| Общее количество тестовых примеров | 29 480 |
| Лучший результат (Top-1 Accuracy) | 60.73% |
| Типы трансформаций | Residual, Witness, Optimization, Set relations, Operator forms |
| Ключевая проблема | Хрупкость формальных знаний при эквивалентных преобразованиях |
Почему это важно
Результаты TREAT указывают на то, что текущие LLM не обладают устойчивым доступом к формальным знаниям. Для областей, требующих строгой валидации (математическое доказательство, верификация кода, научные вычисления), такая «хрупкость» недопустима. Исследование опубликовано в материалах SYNASC 2026 и предлагает новый стандарт для оценки способности ИИ работать с математической сущностью, а не только с текстовыми паттернами.
Источник: arXiv cs.AI ↗