Published on Tue Jan 20 2015

Learning Invariants using Decision Trees

Siddharth Krishna, Christian Puhrsch, Thomas Wies

The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary numerical inequalities.

0
0
0
Abstract

The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one is asked to find a classifier that generalizes from the sample and separates the two sets. Here, the good points are the reachable states of the program, and the bad points are those that reach a safety property violation. Thus, a learned classifier is a candidate invariant. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary Boolean combinations of numerical inequalities. We have used our algorithm to verify C programs taken from the literature. The algorithm is able to infer safe invariants for a range of challenging benchmarks and compares favorably to other ML-based invariant inference techniques. In particular, it scales well to large sample sets.

Mon Jul 06 2020
Machine Learning
Certifying Decision Trees Against Evasion Attacks by Program Analysis
Machine learning has proved invaluable for a range of different tasks, yet it has proved vulnerable to evasion attacks. In this paper we propose a novel technique to verify the security of decision tree models. Our approach exploits the interpretability property of decision trees.
0
0
0
Tue Jul 14 2020
Artificial Intelligence
Verification of ML Systems via Reparameterization
As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. Proof assistants can be used to formally verify machine learning systems by constructing machine checked proofs of correctness.
0
0
0
Wed May 12 2021
Artificial Intelligence
Sufficient reasons for classifier decisions in the presence of constraints
0
0
0
Thu Sep 07 2017
Machine Learning
How Does Knowledge of the AUC Constrain the Set of Possible Ground-truth Labelings?
Data-mining competitions such as Kaggle could potentially be "hacked", either intentionally or inadvertently. For binary classification tasks, one of the most common accuracy metrics is the Area Under the ROC Curve.
0
0
0
Thu May 23 2019
Artificial Intelligence
ENIGMAWatch: ProofWatch Meets ENIGMA
ENIGMAWatch combines two approaches for the given-clause selection implemented for the E ATP system. ProofWatch is motivated by the watchlist (hints) method and based on symbolic matching of multiple related proofs, while ENIGMA is based on statistical machine learning.
0
0
0
Mon May 30 2016
Artificial Intelligence
Internal Guidance for Satallax
We present an efficient scheme for Naive Bayesian classification by generalising label occurrences to types with monoid structure. We implement the method in the higher-order logic prover Satallax, where we modify the delay with which propositions are processed.
0
0
0