TL;DR
Исследование показывает, как модели ошибаются при переписывании математического утверждения из одного «диалекта» в другой. Например, из языка векторных пространств в язык модулей. Ошибка направленная. При переходе к более общей формулировке модель почти всегда молча расширяет область: теряет условие, которое в исходнике было спрятано в самом слове. При переходе к более конкретной формулировке она наоборот сужает область, лишний раз добавляя условие.
Боль в том, что результат выглядит гладко и часто даже остаётся верным там, где его обычно проверяют. Допустим, в тексте было «векторное пространство», а в переписанной версии стало «модуль над кольцом» без слов «кольцо — поле». Формулировка уже говорит о другом классе объектов, но ни проверка на истинность, ни сверка смысла этого не заметят. Причина в том, что модель переносит слова, а условия, спрятанные в словах, не пересчитывает. Более сильная модель делает это чуть реже, но не исправляет ошибку.
Простая инструкция «выпиши все нужные гипотезы» не лечит проблему. Модель начинает чаще упоминать условия, но не лучше понимает, когда они нужны, а когда избыточны. Фраза «стиль оценивать не будут» вообще обнуляет упоминание условий. Практический вывод такой: проверять нужно отдельно истинность, смысл и область утверждения, а не одним вопросом «правильно ли переписано».
Схема метода
В статье нет готового промпта-лекарства. Есть способ проверки, который можно повторить руками в чате:
ШАГ 1: Переписать утверждение в целевой диалект → свежая сессия, без подсказок
ШАГ 2: Проверить истинность одну (без сравнения с исходником) → «истинно» / «ложно + контрпример»
ШАГ 3: Сравнить содержание и область → эквивалентно на общей области? область: = / шире / уже / несравнима
ШАГ 4: Проверить, названо ли скрытое условие → поиск слова-«булавки» в тексте (без LLM-судьи)
Каждый шаг идёт в отдельном запросе. Оценки не усредняются.
Пример применения
Задача: Аспирантка ВШЭ готовит конспект спецкурса. В лекции по линейной алгебре есть теорема «в векторном пространстве всякая система из n линейно независимых векторов — базис, если размерность равна n». Нужно переписать её для модулей над произвольным кольцом, чтобы вставить в лекцию по коммутативной алгебре.
Промпт для шага 3 (в новой сессии, после того как переписанная версия получена):
Ниже два утверждения. Исходное сформулировано для векторных пространств,
кандидат — для модулей над кольцом.
Исходное: {исходное_утверждение}
Кандидат: {переписанное_утверждение}
Ответь строго по пунктам:
1. Над какими объектами квантифицировано исходное утверждение (область)?
2. Над какими — кандидат?
3. Область кандидата: равна исходной / шире / уже / несравнима?
4. Если область отличается — процитируй дословно фразу из кандидата,
где явно записано ограничение. Если такой фразы нет, напиши «нет».
5. Выведи ли исходное из кандидата на общей области? Выведи ли кандидат
из исходного на общей области?
Про истинность кандидата здесь не говори — это отдельный вопрос.
Результат: Модель выдаст пять пронумерованных ответов. Если скрытое условие («кольцо — поле») потеряно, пункт 3 покажет, что область кандидата шире, а в пункте 4 будет «нет». Отдельным запросом про истинность модель скорее всего найдёт контрпример вроде Z/2Z, как в статье.
Почему это работает
Слабость. Модель переписывает утверждение, ориентируясь на слова. В слове «векторное пространство» уже зашито «над полем», и в тексте этого нет. Поэтому при переходе к общему термину условие нужно достать из слова и записать, а при переходе к конкретному — убрать как избыточное. Модель эту операцию, судя по результатам, не выполняет: она копирует уровень общности из исходника.
Сильная сторона. Модель хорошо сравнивает два готовых текста и называет область квантификации, если её прямо об этом спросить. Вопросы про область и про истинность отвечают на разные вещи. Если задать их одним вопросом «насколько верно переписано», ошибка области прячется: утверждение может остаться истинным, но говорить уже о другом.
Как метод использует это. Он разделяет вопросы: истинность отдельно, содержание и область отдельно, наличие скрытого условия проверяется поиском по тексту. Рычаги управления такие: - Свежая сессия на каждый шаг — модель не подстраивается под предыдущий ответ. - Требование «процитируй дословно» — не даёт сказать «условие подразумевается». - Слово-«булавка» (например, «поле», «вероятностная мера», «Set») — ищется глазами или поиском, без LLM-судьи.
Шаблон промпта
Это реконструкция по логике кодирования из статьи. Дословных формулировок авторов в тексте нет.
Ты проверяешь переписанное математическое утверждение. Твоя задача —
не оценить «в целом хорошо», а ответить на отдельные вопросы по очереди.
Исходный диалект: {диалект_A}
Целевой диалект: {диалект_B}
Исходное утверждение: {утверждение_A}
Кандидат (переписанное): {утверждение_B}
Скрытое условие, которое должно было стать явным или уйти: {булавка}
Верно ли кандидат как самостоятельное утверждение?
Вердикт «ложно» допустим только с контрпримером.
e1: выводится ли кандидат из исходного на общей области?
e2: выводится ли исходное из кандидата на общей области?
Область кандидата относительно исходного: = / шире / уже / несравнима.
Если область отличается — процитируй дословно фразу кандидата,
которая записывает ограничение. Нет такой фразы — пиши «нет».
Содержит ли кандидат условие «{булавка}» явно? Да / нет.
Это нужно, если переход идёт к более общему диалекту.
Если переход к более конкретному, отдельно укажи, не добавлено ли
лишнее условие, которое теперь избыточно.
Что подставлять. В {диалект_A} и {диалект_B} — названия областей (например, «линейная алгебра» и «теория модулей»). В {булавка} — условие, которое спрятано в терминах исходника («кольцо скаляров — поле», «мера имеет полную массу 1», «ambient-категория — Set»). Если не знаешь булавку, сначала спроси у модели в отдельном запросе, какие условия подразумевает исходный термин.
🚀 Быстрый старт — вставь в чат:
Вот шаблон проверки переписанного математического утверждения. Адаптируй под мою задачу:
{твоя_задача}. Задавай вопросы, чтобы заполнить поля.
[вставить шаблон выше]
LLM спросит, из какого диалекта в какой идёт перевод и какое условие спрятано в исходных терминах. Без «булавки» шаг 4 нечем проверять. Она возьмёт структуру из шаблона и адаптирует под твою задачу.
Ограничения
⚠️ Узкая область: Исследование про математику, и только про переписывание между вложенными подобластями. Перенос на договоры, ТЗ или код авторы не проверяли.
⚠️ Готового лекарства нет: Добавление одного предложения в промпт не даёт правильного направленного поведения. Инструкция «укажи все гипотезы» повышает частоту упоминаний, но модель чаще оставляет условие и там, где его надо было убрать.
⚠️ Вредные «подсказки»: Фраза, что стиль не оценивается, обнуляет упоминание скрытых условий.
⚠️ Малые выборки на человеческих текстах: Статьи из ProofWiki — всего 25 пар. Часть эффекта там объясняется самой формой записи (условие было набрано явным предложением).
⚠️ Корпус частично искусственный: Основной набор сгенерирован моделью и затем отредактирован. Частоты на «живых» текстах могут быть другими.
⚠️ Проверка не бесплатна: Нужна свежая сессия на каждый шаг и знание того, какое условие спрятано в термине.
Как исследовали
Идея была простой: взять задачу без внешнего «судьи правды». Нельзя прогнать через доказатель или по сумме голосов выбрать лучшее. Исследователи взяли 90 утверждений из готового корпуса MELD (270 пар по девяти областям) по правилу, зарегистрированному заранее. Ещё 45 утверждений оставили нетронутыми для повторной проверки. Добавили 25 пар, написанных математиками, из ProofWiki. Утверждения переписывали семь моделей из четырёх семейств, без системного промпта, при температуре 1, по три попытки. Каждая попытка шла в свежей сессии.
Главное решение дизайна: не сводить качество к одной оценке. Истинность, содержание и область кодировали в отдельных слепых очередях. Отдельно сделали проверку без LLM-судьи: ищут по заранее зафиксированному шаблону, названо ли скрытое условие. Чувствительность метода проверили «подсаженным» контролем: 28 искусственных расширений из 28 были обнаружены.
Результат: при переходе к общему варианту область расширяется примерно в 60% переписываний и ни разу не сужается. При переходе к конкретному сужается примерно в 28% и почти никогда не расширяется. Скрытое условие названо у моделей в 21,6% случаев, у людей-авторов в 4,2%. Это удивило: самая сильная модель расширяет реже всех, но различия между моделями статистически не значимы. Масштаб ошибку не устраняет.
Ещё одна деталь: область сохраняется примерно в половине случаев, где потеря условия сделала бы утверждение ложным. Если же утверждение осталось бы истинным, но про другие объекты, область сохраняется в единицах процентов. Модель сохраняет то, что заметил бы проверяющий на истинность, и теряет остальное. Вывод для практики: проверка «верно ли?» пропустит именно эти ошибки.
Адаптации и экстраполяции
🔧 Техника: проверять каждое направление отдельно → ловить разную ошибку
При переходе к общему варианту проверяй, не потеряно ли условие. Тогда в запрос добавь: «Какое условие подразумевал исходный термин и где оно записано в кандидате?». При переходе к конкретному проверяй, что лишнего не добавлено. Статья показывает, что в двух направлениях ошибки разные.
Экстраполяция (статья этого не проверяла): тот же принцип можно применить, когда модель переписывает юридический шаблон под «любого контрагента» или ТЗ из частного случая в общий. Попроси отдельным запросом: «Какие условия из исходного текста были подразумеваемыми и не записаны в новом?».
Ресурсы
- Статья: Objects Without Morphisms: What LLMs for Mathematics Do Not Represent (препринт).
- Авторы: Yanli Wang (Imperial College London), Xiaopeng Yuan и Haohan Wang (University of Illinois at Urbana-Champaign), Suijin Wang (Tsinghua University).
- Упомянутые в исследовании ресурсы: корпус MELD (Ye et al., 2026), DriftBench (Mohammad & Sheikh, 2026), ProofWiki / NaturalProofs (Welleck et al., 2021), BEq+ (Poiroux et al., 2025).