Formal Methods and Machine Learning

This repository contains a list of research links for the intersection of Formal Methods and Machine Learning.

For applied machine learning for formal methods, some references to machine learning for general software development are included as well, which might be applicable for formal methods. Analogously, articles concerning the verification of arbitrary (black-box) systems are listed, which can be expanded onto machine learning systems.

The entries are (mostly) sorted by publication year (descending), first author (ascending), and title (ascending).

• 1. Applied Machine Learning for Formal Methods
  • 1.1. Tool and Configuration Selection
  • 1.2. Synthesis and Repair
  • 1.3. Formalisation and Specifications
  • 1.4. Feature Selection
  • 1.5. Tooling Analysis and Data Mining
  • 1.6. Model Checking
  • 1.7. Automated Theorem Proving
  • 1.8. Invariant Learning
  • 1.9. Applied ML for General Software Development
  • 1.10. Artificial Intelligence for Formal Software Development
• 2. Applied Formal Methods for Machine Learning
  • 2.1. Neural Networks
  • 2.2. Reinforcement Learning
  • 2.3. Runtime Enforcement and Shield Synthesis
  • 2.4. Markov Chains and Markov Decision Procedures
  • 2.5. Clustering
  • 2.6. Machine Learning Systems
  • 2.7. Cyber-Physical Systems
• 3. Integrated Approaches
  • 3.1. Executable Specifications
  • 3.2. Cyber-Physical Systems
  • 3.3. Planning
  • 3.4. Pattern Recognition
• 4. Unsorted Online Sources
  • 4.1. Courses

1. Applied Machine Learning for Formal Methods

1.1. Tool and Configuration Selection

• "MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers", Scott et al. (2021) [link] [pdf] [doi]
• "Automated Backend Selection for ProB Using Deep Learning", Dunkelau et al. (2019) [link] [pdf] [doi]
• "PaMpeR: Proof Method Recommendation System for Isabelle/HOL", Nagashima & He (2018) [link] [pdf] [doi]
• "Predicting SMT Solver Performance for Software Verification", Healy et al. (2017) [link] [pdf] [doi]
• "Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving", Healy et al. (2016) [link] [pdf] [doi]
• "MUX: Algorithm Selection for Software Model Checkers", Tulsian et al. (2014) [link] [pdf] [doi]
• "Machine learning and automated theorem proving", Bridge (2010) [link] [pdf]
• "ParamILS: An Automatic Algorithm Configuration Framework", Hutter et al. (2009) [link] [pdf] [doi]

1.2. Synthesis and Repair

• "Neural-Backend Generators for Program Synthesis", Bavishi (2019) [link] [pdf]
• "Automatic B-model repair using model checking and machine learning", Cai et al. (2019) [link] [doi]
• "Repair and Generation of Formal Models Using Synthesis", Schmidt et al. (2018) [link] [pdf] [doi]
• "A Supervisory Control Algorithm Based on Property-Directed Reachability", Claessen et al. (2017) [link] [pdf]
• "A theory of formal synthesis via inductive learning", Jha & Seshia (2017) [link] [pdf] [doi]
• "Model Checking-Based Genetic Programming with an Application to Mutual Exclusion", Katz & Peled (2008) [link] [pdf] [doi]

1.3. Formalisation and Specifications

• "A Promising Path Towards Autoformalization and General Artificial Intelligence", Szegedy (2020) [link] [doi]
• "Classifying Non-functional Requirements using RNN Variants for Quality Software Development", Rahman et al. (2019) [link] [pdf] [doi]
• "Machine Learning for Constituency Test of Coordinating Conjunctions in Requirements Specifications", Sharma et al. (2014) [link] [pdf] [doi]
• "Application of reinforcement learning to requirements engineering: requirements tracing", Sultanov et al. (2013) [link] [doi]

1.4. Feature Selection

• "Efficient Semantic Features for Automated Reasoning over Large Theories", Kaliszyk et al. (2015) [pdf]

1.5. Tooling Analysis and Data Mining

• "Analysing ProB's Constraint Solving Backends", Dunkelau et al. (2020) [link] [pdf] [doi]

1.6. Model Checking

• "Using Knowledge Discovery to Propose a Two-phase Model Checking for Safety Analysis of Graph Transformations", Pira (2021) [link] [doi]
• "Locally-Constrained Reinforcement Learning", Hasanbeig et al. (2019) [link] [pdf]
• "LTL Model Checking Based on Binary Classification of Machine Learning", Zhu et al. (2019) [link] [pdf] [doi]
• "Machine Learning Methods in Statistical Model Checking and System Design - Tutorial", Bortolussi et al. (2015) [link] [pdf] [doi]
• "Verification of Markov Decision Processes using Learning Algorithms", Brázdil et al. (2015) [link] [pdf] [doi]
• "Heuristic Model Checking using a Monte-Carlo Tree Search Algorithm", Poulding & Feldt (2015) [link] [doi]
• "Employing AI Techniques in Probabilistic Model Checking Position Paper", Goldman et al. (2014) [link] [pdf]
• "A heuristic solution for model checking graph transformation systems", Yousefian et al. (2014) [link] [pdf] [doi]
• "Bounded Rational Search for On-the-fly Model Checking of LTL Properties", Behjati et al. (2009) [link] [pdf] [doi]
• "Finding Deadlocks in Large Concurrent Java Programs Using Genetic Algorithms", Alba et al. (2008) [link] [pdf] [doi]
• "Exploring very large state spaces using genetic algorithms", Godefroid & Khurshid (2004) [link] [pdf] [doi]
• "Enhancing model checking in verification by AI techniques", Buccafurri et al. (1999) [link] [pdf] [doi]

1.7. Automated Theorem Proving

• "Neural Guidance in Constraint Solvers", Gil Lederman (2021) [link]
• "Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning", Lederman et al. (2020) [link] [pdf]
• "Machine Learning for Instance Selection in SMT Solving", Blanchette et al. (2019) [link] [pdf]
• "A Neurally-Guided, Parallel Theorem Prover", Rawson & Reger (2019) [link] [doi]
• "Guiding High-Performance SAT Solvers with Unsat-Core Predictions", Selsam & Bjørner (2019) [link] [pdf] [doi]
• "Learning A SAT Solver from Single-Bit Supervision", Selsam et al. (2019) [link] [pdf]
• "Reinforcement Learning of Theorem Proving", Kaliszyk et al. (2018) [link] [pdf]
• "Learning Heuristics for Automated Reasoning through Deep Reinforcement Learning", Lederman et al. (2018) [link] [pdf]
• "A Learning-based Fact Selector for Isabelle/HOL", Blanchette et al. (2016) [link] [doi]
• "Learning Rate Based Branching Heuristic for SAT Solvers", Liang et al. (2016) [link] [pdf] [doi]
• "Random Forests for Premise Selection", Färber & Kaliszyk (2015) [link] [pdf] [doi]
• "Learning-assisted theorem proving with millions of lemmas", Kaliszyk & Urban (2015) [link] [pdf] [doi]
• "A Survey of Axiom Selection as a Machine Learning Problem", Blanchette & Kühlwein (2014) [pdf]
• "Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution", Kaliszyk & Urban (2013) [link] [pdf]
• "Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics", Kühlwein et al. (2012) [link] [pdf] [doi]
• "Theorem Proving in Large Formal Mathematics as an Emerging AI Field", Urban & Vyskočil (2012) [link] [pdf] [doi]

1.8. Invariant Learning

• "Synthesizing Environment Invariants for Modular Hardware Verification", Zhang et al. (2020) [link] [pdf] [doi]
• "Quantified Invariants via Syntax-Guided Synthesis", Fedyukovich et al. (2019) [link] [pdf] [doi]
• "Property Directed Inference of Relational Invariants", Mordvinov & Fedyukovich (2019) [link] [pdf] [doi]
• "Accelerating Syntax-Guided Invariant Synthesis", Fedyukovich et al. (2018) [link] [pdf] [doi]
• "Solving constrained hornclauses using syntax and data", Fedyukovich et al. (2018) [link] [pdf] [doi]
• "Quantifiers on Demand", Gurfinkel et al. (2018) [link] [pdf] [doi]
• "Efficiently Learning Safety Proofs from Appearance as well as Behaviours", Prabhu et al. (2018) [link] [pdf] [doi]
• "IC3 - Flipping the E in ICE", Vizel et al. (2017) [link] [pdf] [doi]
• "Learning invariants using decision trees and implication counterexamples", Garg et al. (2016) [link] [pdf] [doi]
• "DeepMath - Deep Sequence Models for Premise Selection", Irving et al. (2016) [link] [pdf]
• "Abstract Learning Frameworks for Synthesis", Löding et al. (2016) [link] [pdf] [doi]
• "ICE: A Robust Framework for Learning Invariants", Garg et al. (2014) [link] [pdf] [doi]
• "Learning Universally Quantified Invariants of Linear Data Structures", Garg et al. (2013) [link] [pdf] [doi]
• "A Data Driven Approach for Algebraic Loop Invariants", Sharma et al. (2013) [link] [pdf] [doi]

1.9. Applied ML for General Software Development

• "Machine Learning for Software Engineering: A Systematic Mapping", Shafiq et al. (2020) [link] [pdf]
• "Awesome Machine Learning On Source Code", [link]

1.10. Artificial Intelligence for Formal Software Development

• "AI meets Formal Software Development", Bundy et al. (2012), [link] [pdf] [doi]

2. Applied Formal Methods for Machine Learning

2.1. Neural Networks

• "Improved Geometric Path Enumeration for Verifying ReLU Neural Networks", Bak et al. (2020) [link] [pdf] [doi]
• "NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems", Tran et al. (2020) [link] [pdf]
• "Verification of Deep Convolutional Neural Networks Using Image Stars", Tran et al. (2020) [link] [pdf]
• "A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees", Wu et al. (2020) [link] [pdf] [doi]
• "A Formalization of Robustness for Deep Neural Networks", Dreossi et al. (2019) [link] [pdf]
• "A Survey of Safety and Trustworthiness of Deep Neural Networks", Huang et al. (2019) [link] [pdf]
• "The Marabou Framework for Verification and Analysis of Deep Neural Networks", Katz et al. (2019) [link] [pdf] [doi]
• "Algorithms for Verifying Deep Neural Networks", Liu et al. (2019) [link] [pdf]
• "Bringing Engineering Rigor to Deep Learning", Pei et al. (2019) [link] [pdf] [doi]
• "Star-Based Reachability Analysis of Deep Neural Networks", Tran et al. (2019) [link] [pdf] [doi]
• "Semantic Adversarial Deep Learning", Dreossi et al. (2018) [link] [pdf] [doi]
• "AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation", Gehr et al. (2018) [link] [pdf] [doi]
• "Reachability Analysis of Deep Neural Networks with Provable Guarantees", Ruan et al. (2018) [link] [pdf]
• "Formal Specification for Deep Neural Networks", Seshia et al. (2018) [link] [pdf] [doi]
• "Formal Security Analysis of Neural Networks using Symbolic Intervals", Wang et al. (2018) [link] [pdf] [video]
• "Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Poly-tope", Wong & Kolter (2018) [link] [pdf]
• "Specification-Guided Safety Verification for Feedforward Neural Networks", Xiang et al. (2018) [link] [pdf]
• "Verification for Machine Learning, Autonomy, and Neural Networks Survey", Xiang et al. (2018) [link] [pdf]
• "Output Range Analysis for Deep Neural Networks", Dutta et al. (2017) [link] [pdf]
• "Safety Verification of Deep Neural Networks", Huang et al. (2017) [link] [pdf] [doi]
• "Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks", Katz et al. (2017) [link] [pdf] [doi]
• "Verifying Properties of BNinarized Deep Neural Networks", Narodytska et al. (2017) [link] [pdf]
• "DeepXplore: Automated Whitebox Testing of Deep Learning Systems", Pei et al. (2017) [link] [pdf]
• "DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars", Tian et al. (2017) [link] [pdf] [doi]
• "Measuring Neural Net Robustness with Constraints", Bastani et al. (2016) [link] [pdf]
• "Towards Verification of Artificial Neural Networs", Scheibler et al. (2015) [pdf]
• "Challenging SMT solvers to verify neural networks", Pulina & Tacchella (2012) [link] [pdf] [doi]
• "An Abstraction-Refinement Approach to Verification of Artificial Neural Networks", Pulina & Tacchella (2010) [link] [pdf] [doi]

2.2. Reinforcement Learning

• "Safe Reinforcement Learning Using Probabilistic Shields", Jansen et al. (2020) [link] [pdf] [doi]
• "Safety Aware Reinforcement Learning (SARL)", Miret et al. (2020) [link] [pdf]
• "Safe Reinforcement Learning via Shielding", Alshiekh et al. (2018) [link] [pdf]
• "Safe Reinforcement Learning via Formal Methods", Fulton & Platzer (2018) [pdf]
• "Safe Model-based Reinforcement Learning with Stability Guarantees", Berkenkamp et al. (2017) [link] [pdf]
• "Safety-Constrained Reinforcement Learning for MDPs", Jungens et al. (2016) [link] [pdf] [doi]
• "A comprehensive survey on safe reinforcement learning", García & Fernández (2015) [link] [pdf] [doi]
• "Reachability-based safe learning with Gaussian processes", Akametalu et al. (2014) [link)] [pdf] [doi]
• "Smart Exploration in Reinforcement LEarning using Absolute Temporal Difference Errors", Gehring & Precup (2013) [pdf]
• "Safe Exploration in Markov Decision Processes", Moldovan & Abbeel (2012) [link] [pdf]
• "Safe Exploration for Reinforcement Learning", Hans et al. (2008) [pdf]

2.3. Runtime Enforcement and Shield Synthesis

• "Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems", Wu et al. (2019) [link] [pdf] [doi]
• "Shield synthesis", Könighofer et al. (2017) [link] [pdf] [doi]
• "Runtime enforcement using Büchi Games", Renard et al. (2017) [link] [pdf] [doi]
• "Shield Synthesis: Runtime Enforcement for Reactive Systems", Bloem et al. (2015) [link] [pdf] [doi]
• "Enforcement of (Timed) Properties with Uncontrollable Events", Renard et al. (2015) [link] [pdf] [doi]
• "Runtime Verification for LTL and TLTL", Bauer et al. (2011) [link] [pdf] [doi]

2.4. Markov Chains and Markov Decision Procedures

• "Smoothed model checking for uncertain Continuous-Time Markov Chains", Bortolussi et al. (2016) [link] [pdf] [doi]
• "Counterexample Explanation by Learning Small Strategies in Markov Decision Processes", Brázdil et al. (2015) [link] [pdf] [doi]

2.5. Clustering

• "A Formal Algorithm for Verifying the Validity of Clustering Results Based on Model Checking", Huang et al. (2014) [link] [pdf] [doi]

2.6. Machine Learning Systems

• "Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking", Chouhan & Banda (2020) [link] [pdf] [doi]
• "Towards Verified Stochastic Variational Inference for Probabilistic Programs", Lee et al. (2020) [link)] [pdf] [doi]
• "Towards Verified Artificial Intelligence", Seshia et al. (2020) [link] [pdf]
• "Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees", Bagnall & Stewart (2019) [link] [pdf] [doi]
• "VerifAI: A Toolkit for the Formal Design and Analysisof Artificial Intelligence-Based Systems", Dreossi et al. (2019) [link] [pdf] [github]
• "On Validating, Repairing and Refining Heuristic ML Explanations", Ignatiev et al. (2019) [link] [pdf]
• "Proving Expected Sensitivity of Probabilistic Programs", Barthe et al. (2018) [link] [pdf] [doi]
• "Grammar Based Directed Testing of Machine Learning Systems", Udeshi et al. (2019) [link] [pdf]
• "The challenge of verification and testing of machine learning", Goodfellow & Papernot (2017) [html]
• "Verification and control of partially observable probabilistic systems", Norman et al. (2017) [link] [pdf] [doi]
• "Developing Bug-Free Machine Learning Systems With Formal Mathematics", Selsam et al. (2017) [link] [pdf]
• "Concrete Problems in AI Safety", Amodai et al. (2016) [link] [pdf]
• "SoK: Towards the Science of Security and Privacy in Machine Learning", Papernot et al. (2016) [link] [pdf]
• "Robustness and generalization", Xu & Manor (2012) [link] [pdf] [doi]

2.7. Cyber-Physical Systems

• "Verification Approaches for Learning-Enabled Autonomous Cyber-Physical Systems", Tran et al. (2020) [link] [pdf] [doi]
• "Vulnerabilities and safety assurance methods in Cyber-Physical Systems: A comprehensive review.", Bolbot et al. (2019) [link] [pdf] [doi]
• "Verising: verifying safety properties of hybrid systems with neural network controllers", Ivanov et al. (2019) [link] [pdf] [doi]
• "Evaluating Model Testing and Model Checking for Finding Requirements Violations in Simulink Models", Nejati et al. (2019) [link] [pdf] [doi]
• "The Logical Path to Autonomous Cyber-Physical Systems", Platzer (2019) [link] [pdf] [doi]
• "Formal Verification of Neural Network Controlled Autonomous Systems", Sun et al. (2019) [link] [pdf] [doi]
• "Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control", Tran et al. (2019) [link] [pdf] [doi]
• "A Systematic Mapping Study on the Verification of Cyber-Physical Systems", Duan et al. (2018) [link] [pdf] [doi]
• "Reasoning about Safety of Learning-Enabled Components in Autonomous Cyber-physical Systems", Tuncali et al. (2018) [link] [pdf] [doi]
• "Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems", Xiang et al. (2018) [link] [pdf] [doi]
• "Work-in-Progress: Testing Autonomous Cyber-Physical Systems using Fuzzing Features from Convolutional Neural Networks", Raj et al. (2017) [link] [pdf] [doi]
• "Integrating Symbolic and Statistical Methods for Testing Intelligent Systems", Ramanathan et al. (2016) [link] [pdf]
• "Modeling and Verifying Intelligent Automotive Cyber-Physical Systems", Jha & Sukthankar (2011) [pdf]

3. Integrated Approaches

3.1. Executable Specifications

• "Labor Division with Movable Walls: Composing Executable Specifications with Machine Learning and Search (Blue Sky Idea)", Harel et al. (2019) [link] [pdf] [doi]

3.2. Cyber-Physical Systems

• "Compositional Falsification of Cyber-Physical Systems with Machine Learning Components", Dreossi et al. (2019) [link] [pdf] [doi]
• "Design and verification of Cyber-Physical Systems using True Time, evolutionary optimization and UPPAAL", Balasubramaniyan et al. (2016) [link] [doi]
• "Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation", Chen et al. (2016) [link] [pdf] [doi]

3.3. Planning

• "Combining Model Checking and Reinforcement Learning for Scalable Mission Planning of Autonomous Agents", Gu et al. (2020) [link] [pdf]

3.4. Pattern Recognition

• "A Formal Methods Approach to Pattern Synthesis in Reaction Diffusion Systems", Gol et al. (2014) [link] [pdf] [doi]

4. Unsorted Online Sources

4.1. Courses

• "Formal Verification Meets Machine Learning", Thomas Noll, Seminar in Theoretical CS, Summer Semester 2018, RWTH Aachen [link]