К автоформализации выходных данных LLM для верификации требований

Основная информация

• ID статьи: 2511.11829
• Название: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• Авторы: Mihir Gupte, Ramesh S. (General Motors)
• Классификация: cs.CL, cs.AI, cs.FL, cs.LO
• Дата публикации: 18 ноября 2025 г. (препринт arXiv)
• Ссылка на статью: https://arxiv.org/abs/2511.11829

Аннотация

В данной работе исследуется возможность применения методов автоматической формализации (Autoformalization) для верификации выходных данных больших языковых моделей (LLM). По мере того как LLM демонстрируют потенциал в преобразовании требований на естественном языке в структурированные выходные данные (например, сценарии Gherkin), возникает критическая проблема: как формально верифицировать точность этих выходных данных. Исследовательская группа провела два набора экспериментов: в первом наборе успешно выявлены логически эквивалентные требования на естественном языке с различными формулировками; во втором наборе обнаружены логические несоответствия между выходными данными LLM и исходными требованиями. Несмотря на ограниченный объём исследования, результаты демонстрируют значительный потенциал автоматической формализации в обеспечении верности и логической согласованности выходных данных LLM.

Исследовательский контекст и мотивация

1. Основная проблема

С распространением приложений LLM, особенно в автоматической генерации тестовых сценариев и других инженерных задач, возникает критический вызов: отсутствие формальных методов для верификации того, что выходные данные LLM точно отражают исходные требования на естественном языке. Например, после генерации сценария Gherkin из требования "Когда скорость автомобиля ≥ 10 км/ч И ремень безопасности не пристёгнут, активировать напоминание о ремне безопасности", невозможно гарантировать логическую корректность сгенерированного содержимого.

2. Значимость проблемы

В критических по безопасности областях, таких как автомобилестроение, верификация требований имеет первостепенное значение. Ошибочное преобразование требований может привести к:

• Неполным или ошибочным тестовым случаям
• Несоответствию поведения системы ожиданиям
• Потенциальным угрозам безопасности

3. Ограничения существующих методов

• Традиционные методы формализации: в основном применяются к доказательству математических теорем, недостаточно используются для верификации инженерных требований
• Методы оценки LLM: полагаются на ручную проверку или эвристические подходы, лишены строгой логической верификации
• Исследования автоматической формализации: сосредоточены на построении наборов данных и обучении моделей, редко применяются к практическим инженерным задачам

4. Исследовательская мотивация

В данной работе предлагается применить методы автоматической формализации к новому сценарию — верификации выходных данных LLM. Подход заключается в преобразовании как требований на естественном языке, так и выходных данных LLM в представление формальной логики (Lean 4) и использовании средства доказательства теорем для верификации логической эквивалентности.

Основные вклады

1. Предложен первый конвейер автоматической формализации для верификации выходных данных LLM: преобразование требований на естественном языке и выходных данных LLM в формальное представление Lean 4 с последующей верификацией логической согласованности посредством доказательства двусторонней эквивалентности
2. Верифицированы два конкретных сценария применения:
   • Выявление логической эквивалентности требований на естественном языке с различными формулировками
   • Обнаружение логических несоответствий между выходными данными LLM и исходными требованиями
3. Выявлены ключевые технические вызовы:
   • Необходимость и сложность автоматизации привязки переменных (variable grounding)
   • Влияние недетерминированности LLM на формализацию
   • Обработка неоднозначности естественного языка
4. Предложены направления будущих исследований: создание основы для построения надёжной системы верификации выходных данных LLM

Подробное описание методов

Определение задачи

Входные данные:

• Пара утверждений (S₁, S₂), требующих верификации логического отношения, которые могут быть:
  • Двумя требованиями на естественном языке
  • Одним требованием на естественном языке и одним сценарием Gherkin, сгенерированным LLM

Выходные данные:

• Определение логической эквивалентности: эквивалентны (можно доказать S₁ ↔ S₂) или не эквивалентны (доказательство не удалось)

Ограничения:

• Утверждения должны быть формализуемы в пропозициональной логике
• Требуется информация о контексте системы для привязки переменных

Архитектура модели

Общий конвейер включает четыре ключевых этапа (см. рисунок 9):

Этап 1: Автоматическая формализация

Использование DeepSeek-Prover-v2 (модель 7B) для преобразования утверждений на естественном языке в пропозиции Lean 4:

-- Пример: формализация требования R1
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

Шаблон подсказки (см. приложение A.1):

• Явное требование генерировать оператор def на Lean 4
• Указание использования пропозициональной логики (тип Prop)
• Требование представления условий в виде импликации (A ∧ B → C)

Этап 2: Привязка переменных (Variable Grounding)

Текущая реализация: ручное выявление и унификация переменных в различных формализациях, указывающих на одну и ту же концепцию

Пример проблемы:

• vehicle_speed_avg в R1 и mean_vehicle_speed в R2 указывают на одну физическую величину
• Необходимо явно указать компилятору Lean об этой эквивалентности

-- Пример ручной привязки
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

Этап 3: Конструирование теоремы двусторонней эквивалентности

Конструирование формальной теоремы для верификации логической эквивалентности:

theorem req1_eq_req2 
  (h_grounding : <предположения о привязке переменных>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <процесс доказательства>

Этап 4: Автоматическое доказательство теорем

Повторное использование DeepSeek-Prover-v2 для генерации кода доказательства Lean:

• Успешное доказательство → два утверждения логически эквивалентны
• Неудача доказательства → существует логическое несоответствие

Технические инновации

1. Инновация в междисциплинарном применении: впервые методы автоматической формализации из области математического доказательства теорем применены к верификации требований в инженерии программного обеспечения
2. Двухуровневое использование LLM:
   • Первый уровень: формализация перевода (ЕЯ → Lean)
   • Второй уровень: доказательство теорем (верификация эквивалентности)
3. Механизм верификации на основе отказа: использование отказа средства доказательства теорем как индикатора логического несоответствия — инновационный метод отрицательной верификации
4. Выявление привязки переменных: явное указание на то, что привязка переменных является неотъемлемым этапом конвейера автоматической формализации, что недостаточно подчёркивалось в предыдущих исследованиях

Экспериментальная установка

Набор данных

Эксперимент 1: Верификация эквивалентности требований

• R1: "If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime"
• R2: "If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt"

Эксперимент 2: Верификация выходных данных LLM

• R3: "When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE."
• G3: Сценарий Gherkin, сгенерированный LLM (содержит 4 примера строк, вводит дополнительные переменные, такие как seat_occupancy)

Метрики оценки

Качественные метрики:

• Успешность/неудача компиляции Lean 4
• Успешность/неудача доказательства теоремы

Критерии верификации:

• Логическая эквивалентность: теорема PA ↔ PB доказуема
• Логическое несоответствие: неудача доказательства теоремы или невозможность компиляции кода Lean

Детали реализации

Выбор модели:

• DeepSeek-Prover-v2 (7B)
• Причины выбора:
  1. Обучена на Lean 4
  2. Обладает способностью понимания естественного языка
  3. Использует стратегию разложения подцелей

Язык формализации: Lean 4

• Мощные возможности доказательства теорем
• Точное выражение логики
• Совместимость с DeepSeek-Prover-v2

Ручное вмешательство:

• Этап привязки переменных полностью ручной
• Верификация выходных данных формализации зависит от компилятора Lean

Результаты экспериментов

Основные результаты

Эксперимент 1: Верификация эквивалентности требований (успешный случай)

Выходные данные формализации:

• R1 и R2 успешно преобразованы в пропозиции Lean (рисунки 3, 4)
• Отображение переменных установлено вручную:
  • vehicle_speed_avg ≡ mean_vehicle_speed
  • seatbelt_active ≡ seatbelt_plugged_in

Результаты верификации (рисунок 5):

• ✅ Компиляция Lean успешна
• ✅ Доказательство теоремы req1_eq_req2 успешно
• Заключение: R1 и R2 логически эквивалентны

Значимость: доказано, что конвейер может выявлять семантически идентичные, но различно сформулированные требования, что способствует проверке согласованности требований.

Эксперимент 2: Верификация выходных данных LLM (случай неудачи)

Выходные данные формализации:

• R3: простая пропозиция, содержит только условие изменения состояния ремня безопасности (рисунок 6)
• G3: сложная пропозиция, содержит дополнительные переменные (seat_occupancy, initial_seatbelt_status) (рисунок 7)

Ключевые находки:

• G3 вводит переменные, не упомянутые в R3
• Логическая структура более сложная (содержит 4 примера сценариев)

Результаты верификации (рисунок 8):

• ❌ Компиляция кода Lean не удалась или доказательство не удалось
• Заключение: G3 логически несовместима с R3

Значимость: успешно обнаружена проблема "чрезмерной генерации" выходных данных LLM — добавление ограничений, отсутствующих в исходном требовании.

Анализ случаев

Случай: Проблема неоднозначности (R4)

Требование:

"When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE."

Проблема: неоднозначность формализации выражения "vehicle in motion"

Две возможные формализации (рисунок 10):

1. pass@1: булева переменная vehicle_in_motion : Bool
2. pass@2: числовая переменная vehicle_speed > 0

Анализ:

• Обе формализации могут быть семантически корректны в контексте системы
• Однако они не эквивалентны в формальной логике (различные типы)
• Подчёркивает влияние неоднозначности естественного языка на формализацию

Экспериментальные находки

1. Формализация зависит от интерпретируемости: недетерминированность LLM приводит к тому, что одно требование может порождать различные, но "разумные" формализации
2. Привязка переменных — узкое место:
   • Наиболее трудозатратный этап
   • Требует знания предметной области системы
   • В настоящее время возможна только ручная реализация
3. Контекст системы критически важен: отсутствие явного определения системы (например, словаря данных) приводит к несоответствиям в формализации
4. Отрицательная верификация эффективна: неудача доказательства эффективно указывает на логическое несоответствие

Связанные работы

Построение наборов данных для автоматической формализации

• ProofNet: автоматическая формализация математики уровня бакалавриата
• MiniF2F: эталон олимпиадной математики
• Многоязычные наборы данных: комбинированное обучение на Lean, Isabelle, Coq повышает производительность

Стратегии обучения LLM

• Метод "черновик-набросок-доказательство" (Jiang et al.): генерация контура доказательства для направления формализации
• Разложение подцелей: рекурсивная стратегия поиска, применяемая DeepSeek-Prover
• Обучение с подкреплением: повышение успешности доказательства теорем

Работа с недетерминированностью

• Структура символической эквивалентности: обработка различий между pass@1 и pass@k
• Методы RAG: извлечение точных формальных определений для предоставления контекста

Расширение в области применения

• Решение математических задач: от средней школы до университета
• Верификация кода: верификация корректности программ
• Биомедицина: проверка фактов

Вклад данной работы: впервые автоматическая формализация применена к верификации инженерных требований и верификации выходных данных LLM, открывая новое направление применения.

Заключение и обсуждение

Основные выводы

1. Верификация возможности: конвейер автоматической формализации может эффективно верифицировать логическую согласованность выходных данных LLM с исходными требованиями
2. Двойная ценность применения:
   • Проверка согласованности требований (выявление эквивалентных требований)
   • Контроль качества выходных данных LLM (обнаружение логических ошибок)
3. Концептуальное доказательство: хотя выборка ограничена, успешно продемонстрирован потенциал применения методов доказательства теорем в инженерии программного обеспечения

Ограничения

1. Ограничения масштаба:
   • Тестирование только 3 пар требований
   • Отсутствие крупномасштабной оценки
   • Отсутствие анализа статистической значимости
2. Зависимость от ручного труда:
   • Привязка переменных полностью ручная
   • Трудозатратна и подвержена ошибкам
   • Ограничивает масштабируемость
3. Ограничения модели:
   • Использование модели 7B (ограничение ресурсов)
   • Более крупные модели (671B) могут показать лучшие результаты
   • Качество формализации зависит от способностей модели
4. Неоднозначность не разрешена:
   • Врождённая неоднозначность естественного языка
   • Отсутствие поддержки системной онтологии
   • Возможность генерации нескольких "корректных", но не эквивалентных формализаций
5. Специфичность для предметной области:
   • Эксперименты ограничены требованиями безопасности автомобилей
   • Способность к обобщению неизвестна

Направления будущих исследований

Статья предлагает три ключевых исследовательских вопроса (RQ):

RQ1: Оптимальный метод формализации

• Исследование стратегии k-pass (генерация нескольких формализаций, выбор наиболее вероятной)
• Сравнение точности однократного преобразования и многократной выборки

RQ2: Автоматизация привязки переменных

• Метод 1: контекстная однократная формализация (обработка всех утверждений в одном вызове)
• Метод 2: привязка на основе сходства (использование встраивания для сопоставления с системной онтологией)
• Вызов: как верифицировать корректность самих предположений о привязке LLM

RQ3: Верификация LLM в системах с ограничениями

• Построение графа знаний действий системы
• Разработка механизма обхода LLM
• Использование автоматической формализации для гарантии логической согласованности выходных данных
• Сценарии применения: умные дома, автомобильные помощники и другие системы с ограниченным пространством действий

Другие направления:

• Разработка методов автоматической нормализации переменных
• Интеграция предметно-ориентированных онтологий (например, словарей данных автомобильных систем)
• Расширение до более сложных логических представлений (например, временная логика)

Глубокая оценка

Преимущества

1. Новизна определения проблемы:
   • Впервые систематически применена автоматическая формализация к верификации выходных данных LLM
   • Решает реальные проблемы инженерной практики
   • Открывает новое направление исследований
2. Ясность методологии:
   • Простой и понятный дизайн конвейера
   • Использование зрелых инструментов (Lean 4, DeepSeek-Prover)
   • Высокая воспроизводимость
3. Глубокое выявление проблем:
   • Ясное указание на критичность привязки переменных
   • Глубокий анализ проблемы неоднозначности
   • Честное обсуждение влияния недетерминированности LLM
4. Высокая практическая ценность:
   • Ориентирована на критические по безопасности области (автомобилестроение)
   • Может быть непосредственно применена в процессе инженерии требований
   • Способствует повышению надёжности приложений LLM
5. Отличное качество написания:
   • Чёткая структура, логичное изложение
   • Подробные шаблоны подсказок (приложение)
   • Богатые иллюстрации, легко понять

Недостатки

1. Критически недостаточный объём экспериментов:
   • Только 3 образца: невозможно сделать статистические выводы
   • Отсутствие тестирования требований различных областей и сложности
   • Не оценена производительность на более крупных наборах данных
   • Рекомендация: требуется как минимум 50-100 пар требований для адекватной оценки
2. Отсутствие количественной оценки:
   • Отсутствуют метрики точности, полноты и т.д.
   • Не сообщается об успешности формализации
   • Отсутствует сравнение с ручной верификацией
   • Рекомендация: создать аннотированный набор данных, вычислить метрики точности
3. Чрезмерное ручное вмешательство:
   • Привязка переменных полностью ручная, подрывает заявления об автоматизации
   • Отсутствуют конкретные реализации решений автоматизации
   • Масштабируемость вызывает сомнения
   • Рекомендация: реализовать хотя бы прототип системы автоматической привязки
4. Ограниченный выбор модели:
   • Использование только модели 7B из-за ограничения ресурсов
   • Не исследованы модели 671B или альтернативные варианты
   • Отсутствует анализ влияния размера модели на результаты
   • Рекомендация: как минимум сравнить различные модели на небольшой выборке
5. Отсутствие анализа случаев неудачи:
   • Не детально проанализированы причины неудачи доказательства теоремы
   • Не различены ошибки формализации и реальные логические несоответствия
   • Отсутствует анализ ложноположительных/ложноотрицательных результатов
   • Рекомендация: разработать систему классификации ошибок
6. Единственный критерий оценки:
   • Только успешность/неудача компиляции Lean
   • Не рассмотрены частично корректные случаи
   • Отсутствует анализ типов ошибок с высокой детализацией
7. Способность к обобщению неизвестна:
   • Тестирование только требований безопасности автомобилей
   • Не верифицирована применимость в других областях (медицина, финансы и т.д.)
   • Специфичность сценариев Gherkin может ограничить универсальность метода

Влияние

Вклад в область:

• ⭐⭐⭐⭐ Концептуальный вклад высокий: предложено новое направление и сценарии применения
• ⭐⭐ Технический вклад средний: в основном комбинация существующих методов
• ⭐⭐⭐ Практическая ценность значительная: решение реальных проблем инженерной практики

Практическая ценность:

• Краткосрочная: предоставление идей верификации инженерам требований
• Среднесрочная: возможное появление специализированных инструментов верификации требований
• Долгосрочная: возможное становление стандартным процессом обеспечения качества приложений LLM

Воспроизводимость:

• ✅ Использование открытых инструментов (Lean 4, DeepSeek-Prover)
• ✅ Предоставлены подробные шаблоны подсказок
• ❌ Код и данные не опубликованы
• ❌ Ручные этапы сложно воспроизвести
• Оценка: ⭐⭐⭐ (средняя)

Ожидаемое влияние:

• Возможное стимулирование дополнительных исследований формальной верификации выходных данных LLM
• Возможное содействие интеграции инженерии требований и формальных методов
• Возможное становление привязки переменных новой горячей темой исследований

Применимые сценарии

Высокая применимость:

• ✅ Верификация требований критических по безопасности систем (автомобили, авиация, медицина)
• ✅ Проверка согласованности требований и дедупликация
• ✅ Контроль качества тестовых случаев, сгенерированных LLM

Средняя применимость:

• ⚠️ Верификация сложной бизнес-логики (требует расширения возможностей формализации)
• ⚠️ Многомодальные требования (например, содержащие диаграммы)
• ⚠️ Системы реального времени (требует расширения временной логикой)

Неприменимо:

• ❌ Высокоамбигуозные тексты на естественном языке
• ❌ Сценарии без явного определения системы
• ❌ Сценарии, требующие ответа в реальном времени (текущие ручные этапы слишком медленны)

Рекомендации по улучшению

1. Немедленно реализуемо:
   • Расширение до как минимум 50 пар требований
   • Реализация базового прототипа автоматической привязки переменных
   • Разработка системы классификации ошибок
2. Краткосрочные улучшения:
   • Сравнение моделей различных размеров
   • Введение количественных метрик оценки
   • Тестирование на нескольких предметных областях
3. Долгосрочные цели:
   • Полная автоматизация конвейера
   • Интеграция графов знаний предметной области
   • Поддержка временной логики и сложных ограничений

Ключевые ссылки

1. Weng et al. (2025): Autoformalization in the era of large language models: A survey — обзорная литература
2. Wu et al. (2022): Autoformalization with large language models — фундаментальная работа по автоматической формализации
3. Ren et al. (2025): DeepSeek-Prover-v2 — основная модель, используемая в работе
4. Jiang et al. (2022): Draft, sketch, and prove — метод разложения подцелей
5. de Moura & Ullrich (2021): The Lean 4 theorem prover — язык формализации

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