3rd Workshop on Learning in VerificationLiVe 2019

We present the Horn-ICE learning, an extension of the classical ICE learning framework. Horn-ICE learning addresses the fact that modern software verification is often highly stylized, and verification conditions often take the form of constrained Horn clauses. We develop a novel learning algorithm for decision trees that operates in this novel setting and show that is is highly effective in learning invariants and contracts of sequential, recursive, and concurrent programs. Moreover, we demonstrate how synthesizing winning strategies for safety games (even on infinite graphs) can be reduced to Horn-ICE learning.

Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. In this talk, we discuss an approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given a temporal logic specification, we synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification.

Besides safety issues, learned controllers have further limitations like: (1) Learned controllers are monolithic and it is not possible to add new features without retraining. (2) When facing un-trained unexpected behavior, the performance of learned controllers might be very poor or it can even result in complete system failure. We address these issues by formalizing deviations from optimal controller performance using quantitative run-time measurements and synthesize quantitative shields that ensure both optimal performance and safe behaviour.

Symmetry is the essential element of lifted inference that has recently demonstrated the possibility to perform very efficient inference in highly-connected, but symmetric probabilistic models models aka. relational probabilistic models. This raises the question, whether this holds for optimization problems in general. In this talk I shall demonstrate that for a large class of mathematical programs this is actually the case. More precisely, I shall introduce the concept of fractional symmetries of linear and convex quadratic programs (QPs), which lie at the heart of many machine learning approaches, and exploit it to lift, i.e., to compress them. These lifted QPs can then be tackled with the usual optimization toolbox (off-the-shelf solvers, cutting plane algorithms, stochastic gradients etc.): If the original QP exhibits symmetry, then the lifted one will generally be more compact, and hence their optimization is likely to be more efficient.

This talk is based on joint works with Martin Mladenov, Martin Grohe, Leonard Kleinhans, Pavel Tokmakov, Babak Ahmadi, Amir Globerson, and many others.

Industries with safety-critical systems increasingly collect data on events occurring at the level of system components, thus cap- turing instances of system failure or malfunction. With data availability, it becomes possible to automatically learn a model describing the failure modes of the system, i.e., how the states of individual components combine to cause a system failure. We present LIFT, a machine learning method for static fault trees directly out of observational datasets, as well as a genetic algorithm to learn fault trees.

The fault trees model probabilistic causal chains of events ending in a global system failure. LIFT makes use of the Mantel-Haenszel statistical test to narrow down possible causal relationships between events. The genetic algorithm is evolutionary in nature; i.e., is an iterative, population-based, randomized search method among fault-tree structures that are increasingly more consistent with the observational data.

We evaluate both algorithms with synthetic case studies, compare their performance at they vary with the quality of the data.

Programming by example is the problem of synthesising a program from a small set of pairs input and output. Despite having found applications in several areas it is notoriously computationally expensive. Recent works have considered hybrid approaches combining ML and PL based techniques. These techniques require generating a training dataset, which leads to significant difficulties related to finding the most informative inputs to characterise a given program.

In this paper we show that the data generation procedure has a significant impact on performance. The novelty of our approach relies on using an SMT solver to synthesize meaningful inputs with varied behaviour for a given program. By testing against several distributions, we show that our constraint-based approach improves on the generalizability of the models. Our results are consistent across two common learning architectures used in previous work.

We study strategy synthesis for POMDPs. The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train a recurrent neural network (RNN) to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory strategy and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications. If the specification is not satisfied, counterexamples supply diagnostic information. We use this information to improve the strategy by iteratively training the RNN. Numerical experiments show that the proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms of solving times and model sizes.

Ongoing work on safety verification of hybrid systems by learning barrier certificates and synthesis of optimal controllers for nonlinear ordinary differential by learning optimal value functions.

Mathematical induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle/HOL. Then, we present MiLkMaId, our approach to suggesting promising applications of mathematical induction without completing a proof search.