Explanation by Automated Reasoning Using the Isabelle Infrastructure Framework

TL;DR

This paper explores using the Isabelle Infrastructure framework for explainable machine learning by formalizing security attack explanations through interactive theorem proving, demonstrating its applicability in dependability engineering.

Contribution

It introduces a novel approach to explainability in machine learning by leveraging formal methods and theorem proving within the Isabelle Infrastructure framework.

Findings

Effective formalization of security attack explanations

Demonstrated applicability in dependability engineering case studies

Showed feasibility of using Isabelle for explainable AI

Abstract

In this paper, we propose the use of interactive theorem proving for explainable machine learning. After presenting our proposition, we illustrate it on the dedicated application of explaining security attacks using the Isabelle Infrastructure framework and its process of dependability engineering. This formal framework and process provides the logics for specification and modeling. Attacks on security of the system are explained by specification and proofs in the Isabelle Infrastructure framework. Existing case studies of dependability engineering in Isabelle are used as feasibility studies to illustrate how different aspects of explanations are covered by the Isabelle Infrastructure framework.