LiVe 2022: 6th Workshop on Learning in Verification
- Held as a satellite event of ETAPS (which we also organize this year!), on April 2, 2022
- Live in Munich! Keep your headsets and webcams at home, come for a real chat;-)
The success of machine learning has recently motivated researchers in formal methods to adapt the highly scalable learning methods to the verification setting, where correctness guarantees on the result are essential.
The aim of this workshop is to bring together researchers from the formal verification community that are developing approaches to exploit learning methods in verification as well as researchers from machine learning area interested in applications in verification and synthesis.
The general topic of machine learning in verification includes, for instance,
the use of learning techniques (e.g. reinforcement learning) for speeding up verification (e.g. rigorous analysis of complex systems combining non-determinism, stochasticity, timing etc.),
the use of machine learning data structures and algorithms (e.g. decision trees) for enhancing results of verification (e.g. generating simple invariants of programs generating small controllers of systems),
verification of machine-learning artefacts (e.g. verification of neural networks), or
- meta-usage of machine learning (e.g. to predict the best tools to be applied to a verification problem).
The 1st edition was held as a satellite event of ETAPS 2017 on April 29, 2017, in Uppsala, Sweden.
It featured 12 presentations and an invited talk by Kim G. Larsen (Aalborg University), who has an ongoing ERC Advanced Grant LASSO (Learning, analysis, synthesis and optimization of cyber-physical systems).
The 2nd edition was held as a satellite event of ETAPS 2018 on April 20, 2018, in Thessaloniki, Greece.
Apart from regular presentations, it featured two invited talks by Guy Katz (Stanford / Hebrew University) and Krishnamurthy Dvijotham (Google DeepMind) on verifying neural networks.
The 3rd edition was held as a satellite event of ETAPS 2019 on April 6, 2019, in Prague, Czech Republic. It included invited talks by Bettina Könighofer and Kristian Kersting and industrial talks by Martin Neuhäusser (Siemens) and Vahid Hashemi (AUDI).
The 4th edition had been postponed together with ETAPS 2020 and took place together with the 5th edition during ETAPS 2021 on March 27, 2021, as a virtual meeting. The invited was delivered by Martin Vechev and Matthew Mirman (both ETH Zurich).
Invited talk will be delivered by
- Armando Tacchella
Title: There is plenty of room at the bottom: verification (and repair) of small-scale learning models
Abstract: With the growing popularity of machine learning, the quest for verifying data-driven models is attracting more and more attention, and researchers in automated verification are struggling to meet the scalability and expressivity demands imposed by the size and the complexity of state-of-the-art machine learning architectures. However, there are applications where relatively small-scale learning models are enough to achieve industry-standard performances, yet the issue of checking whether those models are reliable remains challenging. Furthermore, in these domains, verification is just half of the game: providing automated ways to repair models that are found to be faulty is also an important task in practice. In this talk, I will touch upon some research directions that I have pursued in the past decade, commenting the results and providing some connections with related efforts.
The workshop takes place on site in the room 00.08.038 (ground floor, building segment 8) of the Informatics building of TU Munich, Boltzmnnastr. 3, 85748 Garching, Germany,
on April 2, 2022 (all times CEST).
The inofficial proceedings with all abstracts can be found here.
The discussion document is here.
- Session 1
- 09:00 - 09:20 Opening
- 09:20 - 09:40
Stefan Ratschan: Learning Certificates for Properties of Continuous Dynamical Systems
- 09:40 - 10:00
Eirene V. Pandi, Earl T. Barr, Charles Sutton and Andrew D. Gordon: Type Inference as Optimization
- Session 2 (MDP+RL)
- 10:30 - 10:50
Qisong Yang, Thiago D. Simão, Nils Jansen, Simon Tindemans and Matthijs T. J. Spaan: Training and Transferring Safe Policies in Reinforcement Learning
- 10:50 - 11:10
Steven Carr, Nils Jansen, Sebastian Junges and Ufuk Topcu: Verifiably Safe Reinforcement Learning for POMDPs via Shielding: Probabilistic Type Inference by Optimizing Logical and Natural Constraints
- 11:10 - 11:30
Linus Heck, Jip Spel, Sebastian Junges, Joshua Moerman and Joost-Pieter Katoen: Gradient-Descent for Randomized Controllers under Partial Observability
- 11:30 - 11:50
Marnix Suilen, Thiago D. Simão, Nils Jansen and David Parker: Anytime Learning and Verification of Uncertain Markov Decision Processes
- 11:50 - 12:10
Maximilian Weininger: PAC Guarantees for unknown probabilities through sampling
- 12:10 - 12:30
Debraj Chakraborty, Damien Busatto-Gaston, Shibashis Guha, Guillermo A Pérez and Jean-François Raskin: Safe Learning for Near-Optimal Scheduling
- Session 3 (NN)
- 14:00 - 15:00
Invited talk - Armando Tacchella: There is plenty of room at the bottom: verification (and repair) of small-scale learning models
- 15:00 - 15:20
Marco Sälzer and Martin Lange: Complexity and Decidability Results for Verification of Deep Learning Models
- 15:20 - 15:40
Christopher Brix and Lisa Pühl: Binary-Search Tree Exploration in Verification of Neural Networks
- 15:40 - 16:00
Igor Khmelnitsky, Daniel Neider, Rajarshi Roy, Xuan Xie, Benoit Bardot, Benedikt Bollig, Alain Finkel, Serge Haddad, Martin Leucker and Lina Ye: Formal Verification of Neural Networks by Learning Automata Models
- Session 4 (Properties)
Self-supported workshop dinner
- 16:30 - 16:50
Vahid Hashemi, Jan Kretinsky, Stefanie Mohr, Emmanouil Seferis:
Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks
- 16:50 - 17:10
Simon Lutz, Daniel Neider and Rajarshi Roy: Learning Linear Temporal Formulas from Specification Sketches
- 17:10 - 17:30
Kush Grover, Fernando S. Barbosa, Jana Tumova, Jan Kretinsky: Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments
Since the aim of the workshop is to stimulate discussion on the potential of learning techniques in verification and to report on recent advancements, we invite presentations of possibly already published as well as ongoing work.
The submissions should be abstracts of such work, limited to at most two pages in the llncs style, and will only be published in the informal pre-proceedings for the convenience of the participants. There will be no formal publication or post-proceedings.
The submission are to be done over Easychair.
- Paper submission: February 15, 2022
- Notification: March 1, 2022
- Final versions for informal pre-proceedings: March 10, 2022
In case of any questions, please contact the organizer Jan Kretinsky at <name>.<surname>@tum.de
Looking forward to seeing you LiVe in Munich!