Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Одинаковый ответ Z3 не гарантирует, что языковая модель правильно перевела исходную задачу в формальную логику. Работа Case Western Reserve University и Amazon Web Services показывает AUROC 0,961 для отдельной проверки такого перевода, хотя препринт не рецензирован, а замеры выполнили сами авторы. Для систем с формальным решателем это меняет границу доверия: проверять нужно не только вывод, но и смысл переданной решателю программы.
Верный ответ решателя может скрывать неверный перевод
В нейросимвольной системе языковая модель сначала превращает условие задачи в программу для Z3, а решатель уже доказывает, выполнима ли эта программа. Гарантия Z3 относится только к полученному формальному выражению. Она ничего не говорит о том, сохранила ли модель исходный смысл.
Ошибка может быть почти незаметной: модель меняет знак сравнения, пропускает условие, связывает не ту переменную или разворачивает импликацию. Искажённая программа при этом успешно выполняется и возвращает тот же вердикт, что и правильная.
Авторы называют этот случай сохранением вердикта при неверном переводе. Кандидат должен проходить синтаксическую проверку, совпадать с эталоном по ответу решателя и при этом не быть логически эквивалентным эталону.
На специально подобранных парах проверка только по вердикту не может различить правильный и ошибочный варианты. Её AUROC равен 0,5, то есть качество ранжирования остаётся на уровне случайного выбора. Это узкая граница: она не относится к проверяющим моделям, которые читают исходную задачу, формальную программу или трассу выполнения.
Как GenV перенёс проверку Z3 в языковую модель
При подготовке данных Z3 сравнивает кандидат с эталонной формализацией в обе стороны. Если невозможно найти состояние, где один вариант истинен, а другой ложен, они получают метку эквивалентности эталону (reference-equivalence). Такой тест строже, чем совпадение итоговых вердиктов.
Затем авторы создают трудные отрицательные примеры: меняют оператор, константу или направление импликации. В обучение попадают только правки, которые остаются синтаксически корректными, сохраняют ответ решателя, но меняют логику программы. Это не позволяет модели выучить простой признак вроде ошибки разбора.
GenV построен на языковой модели с 27 млрд параметров. Основные веса заморожены, а обучаемые адаптеры получают исходную задачу и формальную программу. Модель должна ответить одним токеном — Yes или No; нормированные вероятности этих ответов превращаются в непрерывную оценку.
Эталон нужен только во время подготовки меток. В рабочей системе GenV+HN видит исходный текст и кандидатную программу, поэтому его можно поставить после переводчика и перед выбором дальнейшего действия: принять формализацию, запросить новый вариант или выделить больше вычислений.
Основной тест включал 950 формализаций для 197 задач и только реальные ответы моделей-переводчиков, без искусственных мутаций. Из-за совпадений исходных формулировок с обучением авторы отдельно проверили более строгую часть из 652 примеров. Также модель тестировали без дополнительного обучения на других переводчиках и логических стилях из FOLIO, ProofWriter, MALLS, ProverQA, ProntoQA и LogicNLI.
Командам нужен второй контур проверки, а не замена Z3
GenV+HN обошёл голосование по нескольким переводам, которое получило AUROC 0,863. В агентной схеме, где оценка определяла, когда запросить дополнительные варианты формализации, итоговая точность выросла на 11,3 процентного пункта. Простая передача оценки модели как подсказки без расширения числа попыток измеримого выигрыша не дала.
Практический вывод касается архитектуры. Если продукт использует LLM для политик доступа, логических запросов или формальных доказательств, успешный запуск решателя нельзя считать достаточной проверкой. Между переводчиком и решателем нужен контур, который оценивает соответствие исходному тексту и управляет повторными попытками.
При этом GenV не заменяет Z3 и не исправляет программу. Решатель остаётся источником формальной гарантии, а проверяющая модель ранжирует кандидатов и помогает распределять вычисления. Такой контур имеет смысл прежде всего там, где система уже умеет сгенерировать несколько формализаций или повторить перевод при низкой оценке.
Проверка привязана к полностью заданному эталону и строгой логической эквивалентности, а не к субъективному человеческому замыслу. Эксперименты охватывают синтаксически корректные, разрешимые Z3 и выполнимые эталонные спецификации; при сильной смене формального стиля порог оценки может потребовать новой настройки. Поэтому работа меняет схему контроля, но пока не даёт универсального проверяющего слоя для любой формальной системы.
Источники
Иллюстрация: рисунок из статьи «Beyond Solver Verdicts: Generative Reward Models for Autoformalization», Vikash Singh, Debargha Ganguly, Aman Goel и др., CC BY 4.0
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
