Silas: High Performance, Explainable and Verifiable Machine Learning

TL;DR

Silas is a high-performance, explainable, and verifiable machine learning tool that offers formal verification, logical analysis, and transparent decision-making for classification models.

Contribution

Introduces Silas, a classification system with formal foundations, verification modules, and explanation features, enhancing transparency and reliability in machine learning.

Findings

Formal verification of models against user specifications

High-performance implementation of explainable models

Modules for reasoning about and explaining predictions

Abstract

This paper introduces a new classification tool named Silas, which is built to provide a more transparent and dependable data analytics service. A focus of Silas is on providing a formal foundation of decision trees in order to support logical analysis and verification of learned prediction models. This paper describes the distinct features of Silas: The Model Audit module formally verifies the prediction model against user specifications, the Enforcement Learning module trains prediction models that are guaranteed correct, the Model Insight and Prediction Insight modules reason about the prediction model and explain the decision-making of predictions. We also discuss implementation details ranging from programming paradigm to memory management that help achieve high-performance computation.