FMitF: A Novel Framework for Learning Formal Abstractions and Causal Relations from Temporal Behaviors

形式化方法由一组技术组成，这些技术帮助开发人员借助数理逻辑对软件和硬件系统的行为进行严格的推理。虽然形式逻辑已被用于阐明用于验证或软件综合的系统规范，但该项目引入了一个基于逻辑的框架来解决机器学习问题，如分类(新数据应归入哪个类别？)、聚类(应如何将数据点集合组合成类别？)以及发现因果关系(什么时候应该认为较早的数据观察导致了较晚的数据观察的出现？)对于时间序列数据，其中随着时间的推移进行重复观测。形式逻辑的使用开辟了新的途径，例如增强机器学习模型的可解释性，学习结果的可解释性，以及对学习算法行为的形式保证的清晰度。这项工作的社会影响的目标是在医疗保健、自主系统和安全等不同领域的时间序列数据中发现潜在信息。这项研究通过为本科生和研究生提供数据科学、机器学习、形式化方法等领域的跨学科培训，并向学生介绍一些真实世界系统上的统计物理方法来影响教育。该项目探索了基于实时时态逻辑的逻辑推理和机器学习中普遍存在的统计推理之间的交叉。该项目开发的算法允许用户以信号谓词或机会约束的形式表示领域知识，并将分类、聚类或因果发现的结果输出为特定实时时态逻辑中的公式。这允许机器学习算法的结果是人类可解释的，并通过回答为什么特定的时间序列数据以特定的方式被分类或聚类的问题来提高学习算法的可解释性。这些技术能够通过创建一类新的非参数学习方法来对时间序列数据中的不确定性进行建模，该方法结合了统计物理、信息论和统计推理的概念。使用基于逻辑的框架允许通过将可能近似正确的学习(来自计算学习理论)等思想应用于从数据中推断实时时态逻辑公式来为学习过程本身提供形式保证。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Formal methods consist of a collection of techniques that help developers rigorously reason about the behaviors of software and hardware systems with the help of mathematical logic. While formal logic has been used for articulating system specifications for the purpose of verification or software synthesis, this project introduces a logic-based framework to address machine-learning problems such as classification (which category should a new datum be put into?), clustering (how should a collection of data points be grouped together into categories?) and discovery of causal relations (when should an earlier data observation be deemed to cause the appearance of a later data observation?) for time-series data, in which repeated observations are made over time. The use of formal logic opens new avenues such as enhancing the interpretability of machine-learning models, the explainability of learning results, and articulation of formal guarantees on the behavior of learning algorithms. The societal impact of this work targets discovery of latent information in time-series data in diverse domains such as healthcare, autonomous systems, and security. The research impacts education by providing cross-disciplinary training of undergraduate and graduates students in areas of data science, machine learning, formal methods, and introducing students to methods from statistical physics on a number of real-world systems.This project explores the intersection between the logical inference based on real-time temporal logics and statistical inference prevalent in machine learning. The algorithms developed in this project allow users to express domain knowledge in the form of signal predicates or chance constraints, and output the results of classification, clustering or causal discovery as formulas in specific real-time temporal logics. This allows the results of the machine-learning algorithms to be human-interpretable, and also improves the explainability of learning algorithms by answering the question of why a particular time-series datum is classified or clustered in a specific fashion. These techniques are able to model uncertainty in time-series data by creating a new class of non-parametric learning methods that combine concepts from statistical physics, information theory, and statistical inference. The use of a logic-based framework allows providing formal guarantees on the learning process itself by applying ideas such as probably-approximately-correct learning (from computational learning theory) to the inference of real-time temporal logic formulas from data.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.