LLM2Cert верифицирует 81 из 105 сертификатов устойчивости и безопасности

Языковые модели научились писать код и доказывать теоремы. Теперь их пробуют применить к инженерной задаче, где ошибка стоит дорого: подтверждать, что динамическая система остаётся устойчивой и безопасной. Авторы препринта LLM2Cert (arXiv 2610.30524) собрали фреймворк, в котором LLM предлагает сертификаты, а формальные верификаторы их проверяют. На новом бенчмарке DynaCertBench из 105 задач система верифицирует 81, то есть 77,1%. Это на 17,1 процентного пункта больше, чем одноразовая генерация без обратной связи (около 60%).

Почему сертификаты до сих пор остаются узким местом

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

Существующие конвейеры проверяют кандидатов тремя способами: численными солверами (программы sum-of-squares), интервальными методами и SMT-солверами. У всех трёх набор общих проблем. Им нужны релаксации, они консервативны или плохо масштабируются с ростом размерности и нелинейности модели.

Авторы указывают и на побочный эффект. Стандартные тестовые наборы состоят в основном из низкоразмерных полиномиальных систем, подобранных под возможности солверов, а не под потребности инженерии. Бенчмарки отражают то, что умеют инструменты, а не то, что нужно на практике.

DynaCertBench и маршрутизация обязательств

Первая часть работы касается тестового набора. DynaCertBench содержит 105 задач:

• 80 неизбыточных систем, отобранных из литературы;
• расширения этих систем многомерными вариантами и вариантами с ограничениями на управление;
• новые нелинейно связанные системы;
• четыре класса задач: устойчивость, область притяжения (region of attraction), прямая инвариантность (forward invariance) и безопасность.

Вторая часть — сам LLM2Cert. Модель генерирует кандидата в сертификаты, после чего фреймворк раскладывает его на доказательные обязательства. Каждое обязательство направляется по одному из двух путей: в SMT-солвер или напрямую к агенту Lean Proof-Repair. Lean здесь работает как строгий формальный проверяющий, а агент чинит доказательство, если оно не сходится. Именно обратная связь от верификаторов даёт основной прирост: без неё модель, выдающая одного кандидата, закрывает заметно меньше задач.

Цифры, которые стоит держать в голове

• DynaCertBench: 105 задач, из них 80 из литературы.
• LLM2Cert верифицирует 81 из 105 задач, это 77,1%.
• Прирост над one-shot-предложением без обратной связи: 17,1 п.п.
• Из 81 найденного сертификата 22 проверены там, где подход All-SMT, отправляющий всё в SMT-солвер, оставляет вопрос открытым.

Последняя цифра, пожалуй, самая показательная. Это почти четверть сертификатов из набора, до которых чистый SMT не дотягивается. Гибридная маршрутизация закрывает часть задач, с которыми SMT в одиночку не справляется.

Статью подготовили Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue и Alessandro Abate. Код и данные опубликованы в репозитории FormalCert-AI/llm2cert.

Кому это пригодится первым

Практический эффект ожидается там, где управление нелинейными системами требует формальных гарантий: робототехника, автономный транспорт, энергосети, авионика. Инженеру сегодня приходится подбирать сертификат вручную или через SOS-программы, которые упираются в размерность. Схема «LLM предлагает, солвер и Lean проверяют» переносит творческую часть на модель, а доверие оставляет за формальной проверкой. Даже если модель ошибётся, неверный сертификат не пройдёт верификацию.

Для исследователей полезен сам DynaCertBench: на нём можно сравнивать новые методы синтеза на задачах, ближе к реальным системам, чем привычные низкоразмерные полиномы. Открытый код позволяет воспроизвести результаты и подключить другую модель. Остаются 24 задачи из 105, которые LLM2Cert не закрыл, и по ним видно, где у метода пределы.