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

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

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.