论文标题
解释RNN的正式语言方法
A Formal Language Approach to Explaining RNNs
论文作者
论文摘要
本文介绍了Lexr，这是一个使用称为线性时间逻辑（LTL）的正式描述语言来解释复发性神经网络（RNN）决策的框架。 LTL是在形式验证的背景下规范时间属性的事实上的标准，并具有许多理想的属性，使生成的解释很容易解释：它是一种描述性语言，它具有无变量的语言，并且可以轻松地将其翻译成普通的英语。为了产生解释，Lexr遵循反例引导的归纳合成的原理，并将Valiant的近似正确学习（PAC）与约束解决方案相结合。我们证明，Lexr的解释满足PAC保证（前提是RNN可以由LTL描述），并从经验上表明，这些解释比最近从RNN中提取确定性有限自动机产生的解释更准确，更易于理解。
This paper presents LEXR, a framework for explaining the decision making of recurrent neural networks (RNNs) using a formal description language called Linear Temporal Logic (LTL). LTL is the de facto standard for the specification of temporal properties in the context of formal verification and features many desirable properties that make the generated explanations easy for humans to interpret: it is a descriptive language, it has a variable-free syntax, and it can easily be translated into plain English. To generate explanations, LEXR follows the principle of counterexample-guided inductive synthesis and combines Valiant's probably approximately correct learning (PAC) with constraint solving. We prove that LEXR's explanations satisfy the PAC guarantee (provided the RNN can be described by LTL) and show empirically that these explanations are more accurate and easier-to-understand than the ones generated by recent algorithms that extract deterministic finite automata from RNNs.
