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.
翻译:我们考虑了使用人类可解释模型来解释黑盒系统时间行为的问题。为此,基于近年来的研究趋势,我们依赖于确定性有限自动机(DFA)和线性时序逻辑(LTL)公式这两种基础且可解释的模型。与大多数现有的学习DFA和LTL公式的工作不同,我们仅依赖正例。动机在于,负例通常难以观测,尤其是对于黑盒系统。为了仅从正例中学习有意义的模型,我们设计了基于模型简洁性和语言最小性作为正则化器的算法。为此,我们的算法采用了两种方法:符号方法和反例引导方法。符号方法将语言最小性高效编码为约束满足问题,而反例引导方法则通过生成合适的负例来剪枝搜索空间。两种方法都为我们提供了有效的算法,并对学习到的模型给出了理论保证。为了评估算法的有效性,我们在合成数据上对所有算法进行了评估。