Learning Ordered Binary Decision Diagrams (OBDDs) from large-scale datasets is an important topic of explainable artificial intelligence. However, existing search-based methods are still limited in scalability regarding dataset size, since they must explicitly encode the satisfaction of all examples in a dataset. To tackle this challenge, we introduce an OBDD encoding method to parameterize a neural network. This method frees satisfaction encoding of all examples in a dataset while leveraging mini-batch training techniques to enhance learning efficiency. Our main theoretical contribution is to prove that our approach enables the simulation of OBDD inference within a continuous space. Besides, we identify faithful OBDD encoding to fulfill the properties required by OBDDs, allowing to interpret an OBDD directly from the learned parameter assignment. With faithful OBDD encoding, we present an end-to-end neural model named ØBDDNet, being capable of coping with large-scale datasets. Experimental results exhibit better scalability and competitive prediction performance of ØBDDNet compared to state-of-the-art OBDD learners. Valuable insights about faithful OBDD encoding are derived from the ablation study. The implementation is available at: https://github.com/jmq-design/OBDD-NET.

It is important to automatically discover the underlying tree-structured formulae from large amounts of data. In this paper, we examine learning linear temporal logic on finite traces (LTLf) formulae, which is a tree structure syntactically and characterizes temporal properties semantically. Its core challenge is to bridge the gap between the concise tree-structured syntax and the complex LTLf semantics. Besides, the learning quality is endangered by explosion of the search space and wrong search bias guided by imperfect data. We tackle these challenges by proposing an LTLf encoding method to parameterize a neural network so that the neural computation is able to simulate the inference of LTLf formulae. We first identify faithful LTLf encoding, a subclass of LTLf encoding, which has a one-to-one correspondence to LTLf formulae. Faithful encoding guarantees that the learned parameter assignment of the neural network can directly be interpreted to an LTLf formula. With such an encoding method, we then propose an end-to-end approach, TLTLf, to learn LTLf formulae through neural networks parameterized by our LTLf encoding method. Experimental results demonstrate that our approach achieves state-of-the-art performance with up to 7% improvement in accuracy, highlighting the benefits of introducing the faithful LTLf encoding.

We study the problem of learning a single occurrence regular expression with interleaving (SOIRE) from a set of text strings possibly with noise. SOIRE fully supports interleaving and covers a large portion of regular expressions used in practice. Learning SOIREs is challenging because it requires heavy computation and text strings usually contain noise in practice. Most of the previous studies only learn restricted SOIREs and are not robust on noisy data. To tackle these issues, we propose a noise-tolerant differentiable learning approach SOIREDL for SOIRE. We design a neural network to simulate SOIRE matching and theoretically prove that certain assignments of the set of parameters learnt by the neural network, called faithful encodings, are one-to-one corresponding to SOIREs for a bounded size. Based on this correspondence, we interpret the target SOIRE from an assignment of the set of parameters of the neural network by exploring the nearest faithful encodings. Experimental results show that SOIREDL outperforms the state-of-the-art approaches, especially on noisy data.

With the superior learning ability of neural networks, it is promising to obtain highly confident results for linear temporal logic (LTL) satisfiability checking in polynomial time. However, existing neural approaches are limited in inductive ability and in supporting with an arbitrary number of atomic propositions. Besides, there is no mechanism to verify the results for satisfiability checking. In this paper, we propose an approach to checking the satisfiability of an LTL formula and meanwhile generating a satisfiable trace if the LTL formula is satisfiable, where the satisfiable trace verifies the satisfiability result. The core contribution is a new graph representation for LTL formulae - one-step unfolded graph (OSUG) to incorporate the syntax and semantic features of LTL. Preliminary results show that our approach is superior to the state-of-the-art neural approaches on synthetic datasets and confirms the effectiveness of OSUG.

Formal specifications are widely used in software testing approaches, while writing such specifications is a time-consuming job. Recently, a number of methods have been proposed to mine specifications from execution traces, typically in the form of linear temporal logic (LTL). However, existing works have the following disadvantages: (1) ignoring the negative impact of imperfect traces, which come from partial profiling, missing context information, or buggy programs; (2) relying on templates, resulting in limited expressiveness; (3) requesting negative traces, which are usually unavailable in practice. In this paper, we propose PURLTL, which is able to mine arbitrary LTL specifications from imperfect traces. To alleviate the search space explosion and the wrong search bias, we propose a neural-based method to search LTL formulae, which, intuitively, simulates LTL path checking through differentiable parameter operations. To solve the problem of lacking negative traces, we transform the problem into learning from positive and unlabeled samples, by means of data augmentation and applying positive and unlabeled learning to the training process. Experiments show that our approach surpasses the previous start-of-the-art (SOTA) approach by a large margin. Besides, the results suggest that our approach is not only robust with imperfect traces, but also does not rely on formula templates.

Configuration checking (CC) has been confirmed to alleviate the cycling problem in local search for combinatorial optimization problems (COPs). When using CC heuristics in local search for graph problems, a critical concept is the configuration of the vertices. All existing CC variants employ either 1- or 2-level neighborhoods of a vertex as its configuration. Inspired by the idea that neighborhoods with different levels should have different contributions to solving COPs, we propose the probabilistic configuration (PC), which introduces probabilities for neighborhoods at different levels to consider the impact of neighborhoods of different levels on the CC strategy. Based on the concept of PC, we first propose probabilistic configuration checking (PCC), which can be developed in an automated and lightweight favor. We then apply PCC to two classic COPs which have been shown to achieve good results by using CC, and our preliminary results confirm that PCC improves the existing algorithms because PCC alleviates the cycling problem.

Linear temporal logic over finite traces (LTLf) satisfiability checking is a fundamental and hard (PSPACE-complete) problem in the artificial intelligence community. We explore teaching end-to-end neural networks to check satisfiability in polynomial time. It is a challenge to characterize the syntactic and semantic features of LTLf via neural networks. To tackle this challenge, we propose LTLfNet, a recursive neural network that captures syntactic features of LTLf by recursively combining the embeddings of sub-formulae. LTLfNet models permutation invariance and sequentiality in the semantics of LTLf through different aggregation mechanisms of sub-formulae. Experimental results demonstrate that LTLfNet achieves good performance in synthetic datasets and generalizes across large-scale datasets. They also show that LTLfNet is competitive with state-of-the-art symbolic approaches such as nuXmv and CDLSC.

Hai Wan, Haicheng Chen, Jianfeng Du, Weilin Luo, Rongzhen Ye. Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing (Volume 1: Long Papers). 2021.