Lectures by
- Pranav Garg, University of Illinois at Urbana-Champaign
- P. Madhusudan, University of Illinois at Urbana-Champaign
Slides
About
Machine learning [1] has been recently applied to build effective algorithms for problems in verification and synthesis of systems. The first part of the tutorial covers basic machine learning concepts including the different learning problems (in particular, classifiers), various learning models, and known efficient learning algorithms. The second part of the tutorial will focus on how these learning algorithms have been recently adapted [2,3] to solve problems in program verification, with a focus on invariant synthesis. In particular, we will explore new learning models required for invariant generation and synthesis of program expressions, and how traditional machine-learning algorithms can be modified to these new learning models. We will also present a concrete learning algorithm that learns Boolean combinations of Boolean predicates and numerical inequalities that researchers can use to build their own invariant-synthesis engines.
Structure of Tutorial
Introduction: Machine-learning, the classification problem, invariant synthesis, and ICE
Classical classification learning algorithms
Learning conjunctions vs disjunctions; k-CNF; k-DNF
Conjunctions of predicates, Elimination algorithm, Complexity
Linear Threshold Functions: Encoding conjunctions as LTFs, learning small conjunctive formuals and the Winnow algorithm,
Perceptron, SVMs.
Decision trees over Boolean attributes
Decision trees over numerical and Boolean attributes
Adapting classical algorithms to invariant synthesis: ICE and convergence
Extending elimination algorithm for conjuncts to ICE; Houdini
Extending decision-tree learning to ICE
Making decision-tree learning converge, for both (+,-) samples and ICE samples
Open problems
Some invariant synthesis results
Demo on a tool ICE-DT for ICE learning using decision trees
The broader perspective: applying machine learning to more general synthesis problems; challenges.
References
[1] T. M. Mitchell. Machine learning. McGraw Hill series in Computer Science. McGraw-Hill, 1997.
[2] Pranav Garg, Christof Loeding, P. Madhusudan, and Daniel Neider. ICE: A Robust Learning Framework for Synthesizing Invariants, CAV 2014.
[3] Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth. Learning Invariants using Decision Trees and Implication Counterexamples, July 2015.
[4] J.R. Quinlan. Induction on Decision Trees, Machine Learning Vol 1, Issue 1, 1986.
[5] Nick Littlestone. Learning Quickly When Irrelevant Attributes Abound: A New Linear-threshold Algorithm, Machine Learning 285–318(2).