一句话：提出可微神经网络方法 VSCNet，将 LTL 可满足性检验与可满足迹生成（SAT-and-GET）统一为神经推理，兼顾精度与效率。
线性时序逻辑（LTL）可满足性检验具有 PSPACE-完全的高复杂度。近期神经网络方法虽能在多项式时间内近似判定可满足性，却缺乏在判定为可满足时给出可满足迹作为证据的能力，即 SAT-and-GET 问题。本文将该问题桥接到神经网络推理：核心理论贡献是证明精心设计的神经推理过程（称为神经迹检查）能够模拟 LTL 迹检查。基于此提出神经网络方法 VSCNet，借助可微神经迹检查，通过梯度下降同时学习可满足性检验与迹生成。实验验证了 VSCNet 的有效性：相比最先进的神经网络迹生成方法，语义准确率平均最高提升 41.68%；相比最先进的逻辑方法 nuXmv 与 Aalta，在大规模数据集上平均分别取得 186 倍和 3541 倍的加速。
Linear temporal logic (LTL) satisfiability checking has a high complexity, i.e., PSPACE-complete. Recently, neural networks have been shown to be promising in approximately checking LTL satisfiability in polynomial time. However, there is still a lack of neural network-based approach to the problem of checking LTL satisfiability and generating traces as evidence, simply called SAT-and-GET, where a satisfiable trace is generated as evidence if the given LTL formula is detected to be satisfiable. In this paper, we tackle SAT-and-GET via bridging LTL trace checking to neural network inference. Our key theoretical contribution is to show that a well-designed neural inference process, named after neural trace checking, is able to simulate LTL trace checking. We present a neural network-based approach VSCNet. Relying on the differentiable neural trace checking, VSCNet is able to learn both to check satisfiability and to generate traces via gradient descent. Experimental results confirm the effectiveness of VSCNet, showing that it significantly outperforms the state-of-the-art (SOTA) neural network-based approaches for trace generation, on average achieving up to 41.68% improvement in semantic accuracy. Besides, compared with the SOTA logic-based approach nuXmv and Aalta, VSCNet achieves averagely 186X and 3541X speedups on large-scale datasets, respectively.
DOI 原文 ·
@inproceedings{paperbot8471,
title = {Learning to Check LTL Satisfiability and to Generate Traces via Differentiable Trace Checking},
author = {Weilin Luo and Pingjia Liang and Junming Qiu and Polong Chen and Hai Wan and Jianfeng Du and Weiyuan Fang},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3680337}
}