Formal Verification Meets Machine Learning (Seminar)

Seminar in Theoretical CS, Winter 2021/22

News

  • 19.06.2021: we are online

Dates & Deadlines

13.10.2021, 15:30Introduction
20.10.2021Topic preferences due
15.11.2021Detailed outline due
13.12.2021Seminar report due
17.01.2022Presentation slides due
08.-09.02.2022Seminar talks

Introduction and Assignment of Topics

Overview

The term formal verification refers to theory and practice of computer-supported mathematical analysis methods for ensuring correctness of software (and hardware) systems. The modeling and verification of such systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial damage, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality. The latter (additionally) requires proving correctness of systems via automated deduction, e.g., using theorem proving or model checking as a core reasoning method.

A prominent field related to artificial intelligence (AI) is the one of machine learning (ML). Very broadly, machine learning describes algorithms that independently learn from data that is observed in possibly unknown environments. Applications are – only to mention a few – given in autonomous systems, computer vision, and video games. In the real world, these previously not well-defined environments carry the risk of taking safety-critical action along the way of obtaining optimal strategies.

Growing application areas for machine learning, such as autonomous driving, require the exclusion or likely avoidance of unsafe behaviors. An important question is then, how confidence in system behaviors obtained from machine learning can be transferred to formal verification. Vice versa, industrial usage of verification methods such as model checking still suffers from scalability issues for large applications. Leveraging the capabilities of machine learning to assess large data sets will help to enable the verification for more realistic systems. In this seminar, the following approaches will be addressed:

  • Employing learning techniques for software development and verification
  • Safety analysis of deep neural networks

Schedule of Talks

TimeTuesday, February 8Wednesday, February 9
09:00-10:30Nicolay Strohschen, Ziyong Cheong, Moustafa AbdelsalamDominik Geißler, Sven Büge, Nicat Sultanov
11:00-12:30Daniel Buchholz, Constantin Venhoff, Sascha ThiemannAnnika Rüll, Jonas Seidel, Niklas Molczanski
13:30-14:30Daniel Woortmann, Thu Van Dao–

Topics

Approaches to Machine Learning

  1. Introduction to Automata Learning
  2. Introduction to Reinforcement Learning

Learning for Program Verification

  1. Learning Loop Invariants
  2. Model Checking vs. Machine Learning
  3. Reinforcement Learning of Invariants
  4. Termination Analysis of Probabilistic Programs

Learning for Program Synthesis

  1. Programming by Example
  2. Synthesis of Probabilistic Programs
  3. Learning Controllers under Safety Conditions
  4. Combining Program Synthesis and Reinforcement Learning
  5. Deep Learning for Code Synthesis
  6. Learning Programs from Noisy Data
  7. Supervised Learning for Program Correctness

Verification of Deep Neural Networks

  1. An Abstract Domain for Certifying Neural Networks
  2. Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search
  3. Correctness Verification by Tiling
  4. Fast and Precise Certification of Transformers
    • Student: –
    • Supervisor: –
  5. Robustness Certification with Generative Models
    • Student: –
    • Supervisor: –
  6. Provable Repair of Deep Neural Networks
  7. Verifying Recurrent Neural Networks Using Invariant Inference
    • Student: –
    • Supervisor: –
  8. Scalable Polyhedral Verification of Recurrent Neural Networks
    • Student: –
    • Supervisor: –
  9. Property-Directed Verification of Recurrent Neural Networks

Prerequisites

Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic
  • Probability Theory

Previous knowledge in machine learning and semantics of programming languages is helpful but not mandatory

Registration

Registration to the seminar is handled via SuPra. Later registrations are not possible.

Additional Material

Contact

Thomas Noll <noll at cs.rwth-aachen.de>