FMitF: Track I: Formal Methods for Explainable Machine Learning

以机器学习（ML）形式出现的人工智能正在迅速改变世界。今天，机器学习负责越来越多的敏感决策，从贷款决策到疾病诊断，再到自动驾驶。随着ML在许多行业的传播，可解释性的问题，即解释ML中不透明模型的决策，已经占据了中心位置。尽管在可解释性问题上有很多兴趣和进展，但该领域的研究仍处于起步阶段，并没有捕捉到实践中使用的ML模型的全部范围，也没有捕捉到这些模型的用户和主体感兴趣的解释形式。该项目探索了一系列解释任务，这些任务可以由形式方法社区开发的程序合成技术实现（并从中受益）。该项目的影响是为人工智能决策的可解释性奠定逻辑基础，从而有可能确保我们日益自治的世界的透明度。该项目的新颖之处在于使用程序合成以高级程序的形式自动构建简单，连贯，人类可读的解释，ML模型或其决策。该项目研究了对传统（非序列）ML模型和循环模型做出的决策进行可操作解释的综合技术。从技术角度来看，该项目开发了新的程序合成技术，利用优化技术并将其应用于可解释的机器学习所呈现的独特问题设置。其次，该项目开发了用于自动机学习、正则表达式合成和时间逻辑公式合成的算法，并使用它们来解释序列模型的预测。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Artificial intelligence, in the form of machine learning (ML), is rapidly transforming the world. Today, ML is responsible for an ever-growing spectrum of sensitive decisions from loan decisions, to diagnosing diseases, to autonomous driving. With ML spreading across many industries, the issue of explainability, i.e., explaining the decisions of opaque models in ML, has taken center stage. Despite much interest and progress in the explainability question, the research in the area is still nascent and does not capture the full spectrum of ML models used in practice and the forms of explanation that are of interest to users and subjects of those models. This project explores a range of explanation tasks can be enabled by (and benefit from) program-synthesis technology as developed by the formal-methods community. The project's impact is to lay logical foundations for explainability of AI decisions, and thus has the potential to ensure transparency in our increasingly autonomous world. The project's novelty is to use program synthesis to automatically construct simple, coherent, human-readable explanations, in the form of high-level programs, of a ML model or its decisions. The project investigates techniques for synthesizing actionable explanations of the decisions made by a traditional (non-sequence) ML models as well as recurrent models. From a technical viewpoint, this project develops new program-synthesis techniques that leverage optimization technologies and apply them to the unique problem setup presented by explainable machine learning. Second, the project develops algorithms for automata learning, synthesis of regular expressions, and synthesis of temporal-logic formulae and uses them to explain the predictions of sequence models.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.