Sage переводит олимпиадные задачи в Lean 4 и снижает утечку ответов до 2,7%

Нейросетевые системы для доказательства теорем уже показывают впечатляющие результаты, но обычно исходят из того, что корректные формальные утверждения на языке Lean 4 уже даны. Перевод обычной математической постановки в формальный язык остаётся узким местом в данных. По словам авторов статьи, здесь возникает «иллюзия строгости»: стандартные проверки типов пропускают утверждения, которые компилируются, но при этом теряют условия, превращаются в тривиально истинные или незаметно меняют границы в математической постановке.

Чтобы решить проблему, авторы предлагают Sage (Semantic Agent-Guided Formalization Engine), агентный фреймворк. Вместо цельного «одношагового» перевода он использует четырёхэтапный конвейер генерации и цикл семантической коррекции по двум сигналам. Диагностика компилятора Lean 4 объединяется с многомерной семантической обратной связью, так что проверяются и синтаксическая корректность, и математическая верность формулировки.

Отдельно конвейер учитывает разрыв между открытыми вопросами («найдите значение…») и декларативными формальными целями. Из-за этого модели могут показывать высокую долю успешной формализации, просто угадывая непроверенный ответ и вписывая его в утверждение; в аннотации такая утечка ответа указана на уровне 70,9%. Sage снижает утечку до 2,7%.

На наборе Omni-MATH без доказательств Sage достигает 73,3% по метрике pass@4 (совместно учитываются компиляция и смысловая верность) против 42,0% у дообученного базового решения Goedel-Formalizer-V2. Кроме того, авторы собрали IMO-Unformalized, новый набор из 175 ещё не формализованных задач Международной математической олимпиады. Там Sage в режиме zero-shot (без дообучения под набор) показывает 87,4% pass@4 по проверенной верности против 19,4% у базового решения и выигрывает более 79% слепых парных сравнений.

Ключевые факты

Sage (Semantic Agent-Guided Formalization Engine), агентный фреймворк для перевода неформальной математики в утверждения Lean 4: четырёхэтапная генерация плюс цикл семантической коррекции по двум сигналам.
Цикл коррекции сочетает диагностику компилятора Lean 4 с многомерной семантической обратной связью, чтобы ловить утверждения, которые компилируются, но теряют условия или искажают границы.
Утечка ответа, угадывание непроверенного ответа, завышающее долю формализации: в аннотации упомянут уровень 70,9%, Sage снижает утечку до 2,7%.
Omni-MATH без доказательств: 73,3% pass@4 (компиляция и смысловая верность вместе) против 42,0% у дообученного Goedel-Formalizer-V2.
Новый набор IMO-Unformalized из 175 задач Международной математической олимпиады: 87,4% pass@4 проверенной верности против 19,4% у базового решения, более 79% побед в слепых парных сравнениях.

Почему это важно

Системы автоматического доказательства теорем могут работать, только если им дано верное формальное утверждение задачи. Авторы называют перевод с естественного языка в формальный критическим узким местом в данных и показывают, почему простой проверки компиляцией мало: утверждение может скомпилироваться, но потерять гипотезы, стать тривиально истинным или сдвинуть границы. Sage нацелен именно на смысловую верность, а не только на синтаксис. Отдельный вклад, учёт утечки ответа: высокий процент «успешной» формализации можно получить, просто угадав ответ на открытый вопрос и вписав его в утверждение.

Кому это важно

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

Как это применить

Из аннотации видно общий принцип: разбивать формализацию на этапы и замыкать цикл исправления не только на ошибки компилятора, но и на смысловую оценку утверждения. При оценке своих систем стоит отдельно считать утечку ответа на открытых вопросах. О доступности кода, набора IMO-Unformalized или лицензии в аннотации ничего не сказано.

Можно ли доверять

Это препринт на arXiv, а все цифры взяты из аннотации; детали экспериментов в ней не раскрыты. В аннотации не названы авторы и организации, не указаны используемые языковые модели, не перечислены четыре этапа конвейера и измерения семантической обратной связи. Сравнение приведено только с одним базовым решением, Goedel-Formalizer-V2; сравнений с другими системами нет. Не сказано, кто проводил слепые парные сравнения (люди или модели) и сколько их было. Цифра 70,9% в аннотации не привязана к конкретной системе или настройке.

Риски и подводные камни

Результаты получены на двух наборах (Omni-MATH без доказательств и новый IMO-Unformalized), а набор IMO-Unformalized создан самими авторами, и сказано ли о его публикации, неизвестно. Сильный отрыв от базового решения (87,4% против 19,4%) измерен против одного конкурента. Метрика pass@4 означает успех в пределах четырёх попыток, поэтому её нельзя читать как качество первой попытки. Без раскрытия состава оценщиков и числа сравнений вывод о победе в более чем 79% слепых парных сравнений трудно оценить.

«иллюзия строгости»

— авторы статьи, аннотация на arXiv