Magenta связывает математическое рассуждение LLM с проверкой в Lean

Система Magenta научилась выдавать вместе с ответом на олимпиадную задачу доказательство, которое принимает Lean. Хотя препринт не рецензирован и все числа получили сами авторы, Magenta правильно решила 100% задач в основном наборе и сохранила результат после перефразирования условий. Для команд, которые строят проверяемые математические системы, работа предлагает схему надёжнее простого перебора ответов: проверка должна управлять следующим шагом, а не только отбраковывать результат.

Lean проверяет доказательство, но не смысл задачи

Обычная цепочка из LLM и Lean оставляет опасный разрыв. Модель переводит условие на естественном языке в формальное утверждение, после чего Lean проверяет доказательство именно этого утверждения. Если при переводе пропало ограничение, изменилась константа или появилась упрощающая предпосылка, Lean может принять безупречное доказательство не той задачи.

Magenta закрывает этот разрыв отдельной моделью-оценщиком. Сначала модель рассуждает на естественном языке и фиксирует ответ. Формализатор превращает условие и ответ в утверждение Lean 4, а оценщик сравнивает его с исходной задачей. Он должен отклонять формулировки, которые меняют смысл, даже если они корректно записаны.

После этого другая модель строит доказательство, используя неформальное решение как план. Lean проверяет код доказательства, а оболочка SafeVerify не позволяет заменить принятое утверждение или обойти проверку через sorry, новые аксиомы и другие запрещённые конструкции.

Сертификат всё равно остаётся мягким. Ядро Lean гарантирует, что доказано формальное утверждение, но соответствие этого утверждения исходному тексту проверяет LLM, которая тоже может ошибиться. Работа не устраняет смысловой разрыв математически, а ставит перед ним отдельный фильтр и измеряет, насколько тот помогает.

Разделение ошибок предотвращает ложные сертификаты

Основной набор включал 93 задачи из AIME 2025, AIME 2026 и HMMT February 2026. Условия подавали на естественном языке без готовой формальной записи, а ответ во всех этих наборах был числовым. Magenta получила 100% с reasoner-моделями K2-Horizon, Qwen и GPT-5.6-Sol; отдельно K2-Horizon-7B решила все шесть задач IMO 2026.

Главная проверка архитектуры — отключение оценщика формулировки. Тогда система принимала первое утверждение, которое удалось обработать в Lean. Доля ложных сертификатов выросла до 45,5%: почти половина принятых доказательств относилась не к тому ответу, который требовало исходное условие. Формальная проверка без проверки смысла в этом опыте создавала убедительный, но неверно адресованный результат.

Второй оценщик решает, что делать после отказа Lean. Если причина в синтаксисе или реализации доказательства, Magenta сохраняет решение и утверждение, передаёт диагностическое сообщение модели и просит исправить только код. Если ошибка математическая, система возвращает весь контекст модели рассуждения, чтобы та вывела новый ответ.

Такой маршрут оказался полезнее независимых повторных попыток на задачах IMO. Новая выборка доказательства не помогает, когда исходный ответ неверен или когда модель снова попадает в ту же область неудачных решений. Диагностика меняет направление поиска: математическая ошибка запускает новый вывод, а локальная ошибка не заставляет заново решать задачу.

Проверку также повторили на перефразированных условиях AIME 2026, сохранив величины, предпосылки, цель и эталонный ответ. Самостоятельные reasoner-модели стали ошибаться чаще, а связка с Magenta сохранила исходный результат. Такой тест снижает вероятность простого воспроизведения запомненной формулировки, но не исключает утечку полностью: числа в задачах не меняли.

Командам нужен маршрутизатор ошибок, а не ещё один оценщик ответа

Работа меняет архитектурный план для систем, где LLM должна не только предложить математический ответ, но и приложить машинно проверяемое обоснование. Между генерацией формального утверждения и поиском доказательства стоит выделить проверку соответствия. Иначе формальный инструмент подтверждает внутренний артефакт системы, а не пользовательскую задачу.

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

Magenta не требует дополнительного обучения моделей: компоненты связаны подсказками и программным контроллером. Это позволяет испытать подход поверх существующего набора моделей, заменяя reasoner, формализатор или генератор доказательств независимо. Однако переносимость пока показана только на соревновательной математике и Lean, причём основной набор состоит из задач с однозначным ответом.

Работа даёт прототип контура проверки, а не готовую оценку производственной системы. В тексте нет расчёта стоимости и задержки полного прохода, поэтому по нему нельзя выбрать бюджет сервиса. Практический вывод уже применим: сначала стоит проектировать границы сертификата и маршруты исправления, а затем увеличивать число попыток и размер модели.

Источники

• Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Иллюстрация: рисунок из статьи «Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification», Joshua Ong Jun Leang, Haonan Li, Zheng Zhao и др., CC BY 4.0