NeuroNL2LTL: перевод с естественного языка в формальную логику с верификацией до 86%

Группа исследователей опубликовала на arXiv описание NeuroNL2LTL — нейросимволического фреймворка для перевода требований с естественного языка в линейную темпоральную логику (LTL). Работа направлена на повышение надёжности формальной верификации в разработке критически важных систем, таких как авиация, робототехника и беспилотные автомобили.

Традиционные подходы к переводу NL-LTL делятся на два лагеря: шаблонные методы жертвуют выразительностью ради предсказуемости, а нейронные сети дают гибкость, но не гарантируют корректности. NeuroNL2LTL предлагает гибридную архитектуру, где обучение нейросети дополняется формальной проверкой результатов.

Ключевое нововведение — промежуточное представление, которое структурно сохраняет отображение на LTL. Сгенерированные спецификации проходят проверку на выполнимость и нетривиальность. Если выход почти правильный, система применяет минимальный механизм редактирования для исправления ошибок до того, как спецификация попадёт в инструменты верификации.

Центральная идея — обучение с верификатором в цикле: результаты проверки служат сигналом вознаграждения для обучения с подкреплением. Нейронные компоненты оптимизируются непосредственно под формальную корректность, а не под статистическую вероятность. Это позволяет системе учиться на ошибках, которые выявляет верификатор.

На наборе из более чем 200 000 требований из одиннадцати предметных областей (аэрокосмос, робототехника, автономные транспортные средства и др.) NeuroNL2LTL достиг 28% семантической эквивалентности с эталонными спецификациями, а 86% выходов были подтверждены как выполнимые. Система также умеет генерировать контекстуально обоснованные объяснения из LTL, позволяя экспертам в предметной области проверять спецификации без специальной подготовки.

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