Исследователи предлагают циклически согласованную нейронную архитектуру, которая генерирует достоверные естественные языковые объяснения для сертификатов формальной верификации, устраняя непрозрачность этих проверяемых машиной доказательств для неспециалистов. Система достигает 90,0% циклически проверенной корректности на тестовых данных из домена финансового комплаенса, значительно превосходя много-LLM базовые модели как по точности, так и по скорости вывода.
- Архитектура использует прямую сеть (NN1) для отображения сертификатов в объяснения и обратную сеть (NN2) для реконструкции сертификатов, при этом символьный верификатор замыкает цикл для дифференцируемой достоверности.
- Механизм pointer-generator обеспечивает лексическое обоснование путем прямого копирования имен состояний из сертификата; оценка проводилась на 420 тестовых сертификатах, охватывающих шесть методов верификации.
- Модель достигает 90,0% циклически проверенной корректности, превосходя лучшую много-LLM few-shot базовую модель с показателем 76,1% на 13,9 процентных пункта.
- Она выигрывает в 10 из 12 категорий вердиктов/типов, при этом три категории достигают 100% корректности.
- Система обеспечивает скорость вывода в 860 раз выше (185 мс против 160 с), работу офлайн, детерминированные выходные данные и нулевую стоимость на один вывод по сравнению с облачными LLM.
Этот подход демонстрирует, что обученная специализация превосходит использование общих LLM для объяснения структурированных сертификатов, устраняя ограничения развертывания, связанные с облачным выводом.