We address the problem of inferring descriptions of system behavior using
Linear Temporal Logic (LTL) from a finite set of positive and negative
examples. Most of the existing approaches for solving such a task rely on
predefined templates for guiding the structure of the inferred formula. The
approaches that can infer arbitrary LTL formulas, on the other hand, are not
robust to noise in the data. To alleviate such limitations, we devise two
algorithms for inferring concise LTL formulas even in the presence of noise.
Our first algorithm infers minimal LTL formulas by reducing the inference
problem to a problem in maximum satisfiability and then using off-the-shelf
MaxSAT solvers to find a solution. To the best of our knowledge, we are the
first to incorporate the usage of MaxSAT solvers for inferring formulas in LTL.
Our second learning algorithm relies on the first algorithm to derive a
decision tree over LTL formulas based on a decision tree learning algorithm. We
have implemented both our algorithms and verified that our algorithms are
efficient in extracting concise LTL descriptions even in the presence of noise.

该论文提出了两种算法：第一种使用 MaxSAT 求解器在高噪声数据下推导出最小 LTL 公式，第二种算法则基于第一种算法使用决策树学习算法推导出 LTL 公式的决策树。这些算法能够高效地提取简明的 LTL 描述。

从嘈杂数据中学习线性时间属性：一种 MaxSAT 方法

Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach

The wide adoption of machine learning in the critical domains such as medical
diagnosis, law, education had propelled the need for interpretable techniques
due to the need for end users to understand the reasoning behind decisions due
to learning systems. The computational intractability of interpretable learning
led practitioners to design heuristic techniques, which fail to provide sound
handles to tradeoff accuracy and interpretability.
Motivated by the success of MaxSAT solvers over the past decade, recently
MaxSAT-based approach, called MLIC, was proposed that seeks to reduce the
problem of learning interpretable rules expressed in Conjunctive Normal Form
(CNF) to a MaxSAT query. While MLIC was shown to achieve accuracy similar to
that of other state of the art black-box classifiers while generating small
interpretable CNF formulas, the runtime performance of MLIC is significantly
lagging and renders approach unusable in practice. In this context, authors
raised the question: Is it possible to achieve the best of both worlds, i.e., a
sound framework for interpretable learning that can take advantage of MaxSAT
solvers while scaling to real-world instances?
In this paper, we take a step towards answering the above question in
affirmation. We propose IMLI: an incremental approach to MaxSAT based framework
that achieves scalable runtime performance via partition-based training
methodology. Extensive experiments on benchmarks arising from UCI repository
demonstrate that IMLI achieves up to three orders of magnitude runtime
improvement without loss of accuracy and interpretability.

本文提出了 IMLI: 一种基于 MaxSAT 的增量学习方法，通过基于分区的训练方法，实现可扩展的运行时性能，从而在不损失准确性和可解释性的情况下，能够利用 MaxSAT 求解器并处理来自 UCI 存储库的基准测试数据。