Проблема: «Рабочие», но неверные спецификации
Большие языковые модели (LLM) всё чаще используются как формализаторы: они переводят задачи на естественном языке в формальные спецификации для символьных решателей (solvers). Однако возникает парадокс: многие сгенерированные спецификации успешно запускаются, но содержат скрытые логические ошибки — неверные ограничения, домены, предикаты или цели. Поскольку выполнение завершается успешно, обратная связь от решателя не срабатывает, а чистая диагностика на основе LLM часто не выявляет этих ошибок, приводя к ухудшению качества исправлений.
Решение: DRAGO и детерминированная диагностика
Авторы (Giovanni Vaccarino, Emanuele La Malfa и соавторы) предложили фреймворк DRAGO. Его ключевое отличие — замена «незаземленной» критики LLM на детерминированную, специфичную для формализма диагностику. DRAGO принимает исправление только в том случае, если вес диагностированной ошибки строго уменьшается согласно предикату принятия, не требующему эталонного решения (reference-free).
Результаты: Точность и стабильность
Эксперименты проводились на пяти бенчмарках, охватывающих логическое рассуждение (SMT-LIB2), программирование в ограничениях (MiniZinc) и планирование (PDDL). DRAGO демонстрирует значительное улучшение по сравнению с базовыми подходами:
| Метрика | Zero-shot формализация | LLM-диагностика (базовая) | DRAGO (предложенный метод) |
|---|---|---|---|
| Регрессия ошибок (ухудшение качества) | — | 11.8% | 1.3% |
| Рост точности ответов (п.п.) | База | База | +12.9 п.п. (над zero-shot) |
| Рост точности ответов (п.п.) | — | База | +8.7 п.п. (над LLM-диагностикой) |
Снижение регрессии почти на порядок (с 11,8% до 1,3%) делает DRAGO критически важным инструментом для задач, где надежность спецификации важнее скорости генерации.
Скандал в Planetarium: Обнаруженные дефекты
В ходе работы исследователи также выявили серьезные дефекты в датасете Planetarium. Оказалось, что 50% (3 086 экземпляров) разделения на плитки (floor-tile split) не соответствуют эталонным формализациям. Авторы опубликовали исправленное разделение, что важно для всех, кто использует этот бенчмарк для оценки формализаторов.
Значение для индустрии
Результаты показывают, что полагаться исключительно на LLM для создания верифицируемого кода или логики рискованно. DRAGO предлагает гибридный подход: использование вычислительной строгости символьных методов для валидации и исправления, что позволяет сохранить преимущества LLM в генерации, но избежать их главных слабостей в логической точности.
Источник: arXiv cs.AI ↗