Модель знает теорему — пока её не переписали другой формулой

Самая неприятная проблема с математическими моделями может быть не в незнании теорем, а в хрупком доступе к ним. В тесте TREAT лучшая модель правильно определяла теорему лишь в 60,73% случаев, когда её условие переписывали в эквивалентной форме.

То есть смысл утверждения сохранялся, но менялась оболочка: вместо стандартной записи появлялись остаточные уравнения, условия существования свидетеля, оптимизационные тождества, отношения множеств или операторные формы. Для человека, знакомого с предметом, это разные дороги к одному объекту. Для модели — иногда уже другая задача.

TREAT проверяет именно распознавание идентичности теоремы. В наборе 737 теорем и 29 480 преобразованных примеров, причём для каждого варианта сохранены исходные предположения и обратное отображение к канонической формулировке. Это полезнее обычного теста на пересказ: модель не может отделаться похожими словами и должна понять, что перед ней тот же формальный результат.

Практический вывод простой: если AI-система должна передавать знания в Mathematica, Lean, Coq или другой формальный инструмент, нельзя проверять её только на привычных формулировках. Нужны эквивалентные представления, явные проверки и возможность честно сказать «не знаю», вместо уверенного ответа не по адресу.

Но у теста есть границы. Он построен на теоремах, собранных со страниц с математическими выражениями, и проверяет восстановление имени теоремы, а не доказательство, корректность вывода или способность решать новую задачу. Кроме того, системы ошибались по-разному: отказывались отвечать, выбирали неверную теорему или выдавали плохо сформированный результат. Поэтому 60,73% — не оценка «математического интеллекта» вообще, а показатель хрупкости в конкретном, хорошо контролируемом сценарии.

Если вы используете AI для технической работы, что для вас опаснее: ошибка в рассуждении или уверенное узнавание знакомого ответа только потому, что задача записана в привычной форме? Источник: cs.AI updates on arXiv.org