Explanation by Automated Reasoning Using the Isabelle Infrastructure Framework
This work addresses the need for formal explanations in machine learning, particularly for security applications, but appears incremental as it builds on existing case studies in dependability engineering.
The paper tackles the problem of explainable machine learning by proposing interactive theorem proving, specifically using the Isabelle Infrastructure framework, to explain security attacks through formal specification and proofs.
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.