Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Систему научили превращать неявные доводы из обычного текста в формальные доказательства и отказываться от ответа, если для доказательства приходится искажать исходный аргумент. В работе Xin Quan, Reto Gubelmann и André Freitas, которая не прошла рецензирование и приводит замеры самих авторов, GUARD обошёл сильнейший базовый метод на 32,9–35,3 процентного пункта. Для подобных систем одного подключения LLM к решателю недостаточно: между ними нужен отдельный слой допущений и проверок на подмену смысла.
Как GUARD достраивает скрытый переход
На входе система получает посылку и утверждение, которое она должна поддерживать. В естественном языке между ними часто не хватает правила: например, читатель сам понимает, почему устойчивость сельскохозяйственной культуры к болезням может увеличить урожай, но формальный решатель такого знания не предполагает.
GUARD сначала строит расширенный контекст из трёх типов элементов. Допущения задают нормальные условия, область применения и скрытые основания аргумента. Определения связывают разные формулировки одного понятия, а исключения описывают случаи, когда обычное правило перестаёт работать.
Из расширенного контекста LLM выбирает набор условий, нужных именно для данного перехода. Они становятся аксиомами, посылка — предпосылкой теоремы, а утверждение — целью доказательства. Исключения входят в правила явно: вывод действует, только если не сработало условие, которое его блокирует.
Затем LLM переводит предложения в логику первого порядка, сохраняя участников событий и связи между ними. До запуска Isabelle/HOL отдельная модель-критик проверяет четыре свойства: корректность формальной записи, достаточность условий, возможность вывести утверждение и зависимость доказательства от каждого выбранного условия.
Isabelle/HOL выполняет жёсткую проверку. Если доказательство останавливается, GUARD извлекает не общий вердикт, а конкретный неудавшийся шаг и использованные аксиомы. LLM получает этот фрагмент, исправляет логическую форму или набор условий и снова отправляет теорию решателю. Так обратная связь указывает на локальный разрыв, а не предлагает модели переписать всё объяснение.
Почему доказуемость ещё не означает верность
Свободно добавляя аксиомы, система может доказать почти любое утверждение. Условие способно прямо повторить требуемый вывод, сделать исходную посылку ненужной или оказаться настолько широким, что из него следуют соседние утверждения на ту же тему. Isabelle/HOL подтвердит такую теорию: логически она корректна.
GUARD поэтому проверяет уже доказанную теорию на контрастных примерах. Сначала он убирает исходную посылку или заменяет её другой посылкой на ту же тему, которая не поддерживает вывод. Если доказательство сохраняется, добавленные условия содержат ответ или обходят исходный довод.
Вторая проверка оставляет посылку, но подменяет вывод близким по теме утверждением. В примере с устойчивыми к болезням культурами посылка может поддерживать пользу через рост урожая, но не доказывает безопасность продукта для потребителей. Если теория выводит и безопасность, набор условий захватил больше смысла, чем было в аргументе.
Система принимает результат только тогда, когда исходное доказательство проходит, а все подменённые варианты становятся недоказуемыми. Иначе она сужает условия и повторяет проверку. Если допустимое исправление не найдено, GUARD различает нехватку условий и несовместимость посылки с утверждением, вместо того чтобы выдавать формально удобное объяснение.
Что меняется в планах команд
На Debatepedia и ARCT система с GPT-5.1 получила 76,5% и 81% доказательств, которые одновременно прошли решатель и контрастные проверки. Доля формально доказанных, но смыслово протекающих результатов не превысила 2,1%. Удаление предварительной критики снижало итоговый показатель примерно на 40 пунктов, а удаление слоя допущений — до 31,5 пункта.
Результат повторился с GPT-5.1, Qwen3-Max, DeepSeek-V3.2 и Mistral Medium 3.5. Проверяли аргументы из Debatepedia и ARCT, где уже заданы пары «посылка — утверждение» и требуется восстановить скрытое основание. Эти замеры подтверждают подход для коротких аргументативных переходов; перенос на другие области авторы оставили дальнейшей работой.
Если продукт должен не просто генерировать объяснение, а проверять, действительно ли оно следует из исходных данных, архитектуру стоит разделить на явные этапы. Сгенерированные допущения нужно хранить отдельно от входного текста, проверять решателем и испытывать подменой посылки и вывода. Статус отказа также становится частью результата, а не ошибкой, которую следует любой ценой заменить ответом.
Работа не показывает, что формальный решатель сам устраняет выдуманные предпосылки. Основной выигрыш дал слой перед Isabelle/HOL: он формулировал недостающие условия, исправлял представление и удалял лишние аксиомы. Поэтому простой цикл «LLM написала доказательство — решатель подтвердил» остаётся уязвимым к корректной по форме, но подогнанной теории.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
