Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Fyan научился находить расхождения между исходной математической формулировкой и теоремой на Lean до того, как следующая часть документа начнёт на неё опираться. В нерецензированном препринте, где все числа получили сами авторы, система доказала со строгой проверкой Lean 86 из 143 теорем против 69 у универсального агентного процесса. Для команд, которые автоматизируют формализацию документов, работа предлагает отделить генерацию доказательств от допуска теорем в библиотеку.
Проверенное доказательство не гарантирует верный перевод
Lean проверяет, следует ли вывод из формальной постановки, но не сверяет эту постановку с исходным текстом. Модель может убрать условие, изменить область переменной или подменить математический объект, а затем построить безупречное доказательство уже другой теоремы.
На уровне документа такая ошибка распространяется дальше. Последующие теоремы импортируют проверенный модуль, поэтому весь проект продолжает собираться, хотя часть результатов больше не соответствует источнику.
Fyan разделяет три задачи: правильно понять исходную формулировку, построить доказательство и проверить получившийся код средствами Lean. Модель может предлагать решения на каждом этапе, но переход между этапами разрешают отдельные проверяемые правила.
Исходный документ сначала разбивают на самостоятельные теоремы и связывают их графом зависимостей. Теоремы обрабатывают по порядку: готовые модули становятся зависимостями для следующих, а постановка и план доказательства остаются защищёнными от незаметного редактирования во время поиска.
Как семантический аудит находит потерянное условие
Перед поиском доказательства Fyan сопоставляет исходную формулировку с кандидатом на Lean. Языковая модель выделяет объекты, гипотезы, выводы, области действия и используемые определения, цитирует подтверждающие фрагменты источника и описывает соответствия между элементами.
Вердикт принимает не сама модель. Детерминированный валидатор проверяет, все ли элементы сопоставлены, совпадают ли области действия переменных, допустимо ли направление логического изменения и достаточно ли приведённых свидетельств. Итоговый класс задаёт худшее найденное расхождение, поэтому несколько точных соответствий не могут скрыть одно пропущенное условие.
Если источник требует одновременно x > 0 и x < 1, а формальная теорема сохраняет только первое условие, второе остаётся несопоставленным. Система возвращает постановку на исправление и указывает, что именно потеряно, вместо общего ответа о несогласованности.
Некоторые изменения допустимы только в одном направлении. Кандидат может использовать более слабые предпосылки или доказывать более сильный вывод, если из его доказательства можно восстановить исходную теорему. Однако семантический аудит не объявляет такую постановку равной источнику.
По умолчанию содержательно изменённую формулировку отправляют на исправление. Если команда разрешает принять её, Fyan создаёт исходно ориентированную постановку и требует доказать в Lean переход S1 → S0: от принятого кандидата к версии, которая отражает источник. Этот мост проверяет формальный перенос доказательства, а соответствие S0 исходному тексту снова проходит семантический аудит.
Командам нужен новый контур приёмки, а не другая модель
На ConsistencyCheck аудит проверяли на 300 парах формулировок. Полнота — доля найденных несогласованных примеров — составила 0,777 против 0,636 у прямого ответа той же модели. Главное практическое отличие состоит не только в более высокой метрике: отчёт привязывает ошибку к конкретной гипотезе, выводу или области действия, поэтому формализатор получает локальную задачу на исправление.
Работу проверяли с DeepSeek-V4.1-Flash на всех этапах и сравнивали с универсальным агентным процессом при том же окружении Lean и тех же средствах оценки. Документный сценарий показан на ODENumLib: библиотека включает 20 связанных зависимостями теоремных блоков и 9 355 строк Lean по численным методам для обыкновенных дифференциальных уравнений.
Масштаб результатов пока задают одна модель, математические задачи и один предметный проект. Аудит также требует больше обращений к модели, чем прямой бинарный вопрос о соответствии, поэтому его разумнее ставить на границе допуска в библиотеку, а не после каждого чернового шага.
Работа меняет архитектурный план систем формализации документов. Состояние процесса стоит хранить в постоянных артефактах, постановку замораживать до поиска доказательства, а допуск следующей зависимости отдавать детерминированному шлюзу. Если изменение смысла действительно нужно, оно должно оставлять проверяемое обязательство переноса, а не пояснение модели в журнале.
Это не устраняет необходимость человеческой проверки источника: языковая модель по-прежнему формирует семантические свидетельства. Но ошибка становится локализованной и не может пройти дальше только потому, что код компилируется и доказательство принято ядром Lean.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
