Certified Verification with Applications

What it is

The focus of the seminar series is to build a bridge between research groups in Kaiserslautern with interests in formal verification, machine learning, distributed systems, and embedded systems, oriented towards the topic of certified verification. The past decades have seen the rise of powerful methods in formal verification and machine learning, including SAT and SMT-solvers, deep neural networks, program synthesis, and property-directed reachability (IC3), to mention a few. Such techniques, as well as the optimizations that are applied to increase scalability and applicability, often become so complex that bugs in those implementations start to creep in. We are interested in techniques that can ensure correctness in those implementations, including certified solvers, certified verifiers, and type systems, among others. The aim of the seminar series is to exchange ideas that could lead to the development of such techniques.

Involved groups

When and where

  • Online via Zoom
  • Date and time: Thursdays 13:00
  • Check the schedule below for exact dates.
  • A longer-term plan can be found in this Google Calendar.

Interested?

  • To get the Zoom link of the next talks, please subscribe to the seminar's mailing list as follows:
  • Write a mail to sympa@informatik.uni-kl.de with subject "subscribe arg-cervera Yourfirstname Yourlastname" and empty message body.
  • If you have any questions, feel free to contact Pascal Bergsträßer (bergstraesser[at]cs.uni-kl.de).

Next talk

  • 22.04.21: Talk by Pablo Barceló
    • Title: Explainability Queries for ML Models and its Connections with Data Management Problems
    • Abstract:
      In this talk I will present two recent examples of my research on explainability problems over machine learning (ML) models. In rough terms, these explainability problems deal with specific queries one poses over a ML model in order to obtain meaningful justifications for their results. Read Less Both of the examples I will present deal with “local” and “post-hoc” explainability queries. Here “local” means that we intend to explain the output of the ML model for a particular input, while “post-hoc” refers to the fact that the explanation is obtained after the model is trained. In the process I will also establish connections with problems studied in data management. This with the intention of suggesting new possibilities for cross-fertilization between the area and ML. The first example I will present refers to computing explanations with scores based on Shapley values, in particular with the recently proposed, and already influential, SHAP-score. This score provides a measure of how different features in the input contribute to the output of the ML model. We provide a detailed analysis of the complexity of this problem for different classes of Boolean circuits. In particular, we show that the problem of computing SHAP-scores is tractable as long as the circuit is deterministic and decomposable, but becomes computationally hard if any of these restrictions is lifted. The tractability part of this result provides a generalization of a recent result stating that, for Boolean hierarchical conjunctive queries, the Shapley-value of the contribution of a tuple in the database to the final result can be computed in polynomial time. The second example I will present refers to the comparison of different ML models in terms of important families of (local and post-hoc) explainability queries. For the models, I will consider multi-layer perceptrons and binary decision diagrams. The main object of study will be the computational complexity of the aforementioned queries over such models. The obtained results will show an interesting theoretical counterpart to wisdom’s claims on interpretability. This work also suggests the need for developing query languages that support the process of retrieving explanations from ML models, and also for obtaining general tractability results for such languages over specific classes of models.
    • Bio:
      Full Professor at Pontificia Universidad Católica de Chile, where he also acts as Director of the Institute for Mathematical and Computational Engineering. He is the author of more than 80 technical papers, has chaired ICDT 2019, will be chairing ACM PODS 2022, and is currently a member of the editorial committee of Logical Methods in Computer Science. From 2011 to 2014 he was the editor of the database theory column of SIGMOD Record. His areas of interest are database theory, logic in computer science, and the emerging relationship between these areas and machine learning.
  • 15.04.21 06.05.21: Talk by Yunwen Lei
    • Title: Statistical Learning by Stochastic Gradient Descent
    • Abstract:
      Stochastic gradient descent (SGD) has become the workhorse behind many machine learning problems. Optimization and sampling errors are two contradictory factors responsible for the statistical behavior of SGD. In this talk, we report our generalization analysis of SGD by considering simultaneously the optimization and sampling errors. We remove some restrictive assumptions in the literature and significantly improve the existing generalization bounds. Our results help to understand how to stop SGD early to get a best statistical behavior.
    • Bio:
      Dr. Yunwen Lei got his PhD degree from Wuhan University in 2014. He is now a Lecturer at School of Computer Science, University of Birmingham. Previously, he was a Humboldt Research Fellow at University of Kaiserslautern, a Research Assistant Professor at Southern University of Science and Technology, and a Postdoctoral Research Fellow at City University of Hong Kong. Dr. Lei's research interests include learning theory and optimization. He has published papers in ICML, NeurIPS, ICLR and some prestigious journals including IEEE Transactions on Information Theory and Journal of Machine Learning Research.

Past talks

  • 25.03.21: Talk by Oliver Markgraf
    • Title: Learning in reactive Synthesis
  • 18.03.21: Talk by Chih-Hong Cheng
    • Title: Verification and Validation of DNN-based Autonomy Perception
  • 11.03.21: Talk by Ekaterina Komendantskaya
    • Title: Continuous Verification of Machine Learning: a Declarative Programming Approach
  • 25.02.21: Talk by Yutaka Nagashima
    • Title: Artificial Intelligence for Inductive Theorem Proving
  • 11.02.21: Talk by Dave Parker
    • Title: Verification with Stochastic Games: Advances and Challenges