Исследователи EleutherAI и их коллеги представили SemantEq — способ проверять, сохранил ли перевод математического утверждения на язык Lean его смысл. В препринте от 23 октября отдельная программа проверки отклонила все 104 пары утверждений, которые авторы признали разными по смыслу. При двух вариантах инструкции для примерно двух пятых этих пар ИИ сумел написать формально корректные доказательства взаимного следования.

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

SemantEq ограничивает допустимые переходы между формулировками: например, перестановкой логических частей или переписыванием через равенства из математической библиотеки. Программа разбирает само доказательство, проверяемое Lean, и смотрит, действительно ли в нём использовалось другое утверждение. В одном варианте переходы ищет обычная программа без языковой модели; в другом ИИ предлагает доказательства, а SemantEq-ProofAudit отдельно решает, принять ли их.

В опыте с GPT-5.6 Sol в Codex проверка приняла 330 из 407 действительно равнозначных пар — 81,1% при лучшем из четырёх вариантов инструкции, против 266 пар, или 65,4%, у поиска без модели. Ни одну из 104 неравнозначных пар аудитор не пропустил. Это результат самих авторов на выборке с пересмотренной ими разметкой, с одной моделью и одним сеансом на пару и вариант инструкции. Он не означает, что любые доказательства ИИ теперь проверяются безошибочно: у варианта поиска без модели авторы отдельно описали ложное принятие на другой части данных.

Код опубликован под Apache 2.0. Для работы всё ещё нужна доверенная формулировка-эталон на Lean: если ошибка уже в ней, совпавший с ней перевод тоже пройдёт. Поэтому SemantEq добавляет проверку соответствия эталону, а не заменяет проверку математиком исходной задачи. На фоне перевода больших доказательств в машинно проверяемый код это существенное различие: компьютерная проверка логики и сохранение смысла поставленной задачи — два отдельных требования.