论文标题
仅从积极示例中学习可解释的时间属性
Learning Interpretable Temporal Properties from Positive Examples Only
论文作者
论文摘要
我们考虑使用人解剖模型来解释黑盒系统的时间行为的问题。为此,根据最近的研究趋势,我们依靠确定性有限自动机(DFA)和线性时间逻辑(LTL)公式的基本但可解释的模型。与学习DFA和LTL公式的大多数现有作品相反,我们仅依靠积极的例子。我们的动机是,通常很难从黑盒系统中观察到负面例子。仅从积极的示例中学习有意义的模型,我们设计了依赖于模型作为正规化器的简洁性和语言最小值的算法。为此,我们的算法采用了两种方法:一种符号和反例引入的方法。尽管符号方法利用语言最小值作为约束满意度问题的有效编码,但反例引入的人依赖于生成合适的负面例子来修剪搜索。两种方法都为我们提供了有效的算法,并在学习模型上具有理论保证。为了评估算法的有效性,我们在合成数据上评估了所有算法。
We consider the problem of explaining the temporal behavior of black-box systems using human-interpretable models. To this end, based on recent research trends, we rely on the fundamental yet interpretable models of deterministic finite automata (DFAs) and linear temporal logic (LTL) formulas. In contrast to most existing works for learning DFAs and LTL formulas, we rely on only positive examples. Our motivation is that negative examples are generally difficult to observe, in particular, from black-box systems. To learn meaningful models from positive examples only, we design algorithms that rely on conciseness and language minimality of models as regularizers. To this end, our algorithms adopt two approaches: a symbolic and a counterexample-guided one. While the symbolic approach exploits an efficient encoding of language minimality as a constraint satisfaction problem, the counterexample-guided one relies on generating suitable negative examples to prune the search. Both the approaches provide us with effective algorithms with theoretical guarantees on the learned models. To assess the effectiveness of our algorithms, we evaluate all of them on synthetic data.