Pôle Interactions Formal Methods for Artificial Intelligence

Contact: Benedikt Bollig

Topics

The team is concerned with topics at the interface between formal methods and artificial intelligence:

  • Reasoning about knowledge: We study logical formalisms that have applications in planning, synthesis, or formalizing the strategic behavior of intelligent agents (e.g., description logics, strategy logics, fuzzy logic, and dynamic logics).
  • Robust and verified AI and ML: Formal methods can help develop robust, verified, and explainable AI and machine-learning components. In particular, we exploit model learning to extract structural information from recurrent neural networks.
  • Application of ML algorithms: We use machine learning to synthesize algorithms (e.g., controllers in cyber-physical systems) and to identify system parameters (e.g., in bio-chemical reaction networks).

News

Stéphane Demri (LMF, CNRS) and Karin Quaas (Leipzig University) won the Best-Paper Award at JELIA 2023 for their article First Steps Towards Taming Description Logics with Strings.

Working Group

We regularly welcome speakers to talk about AI-related topics. Usually, talks take place on Friday at 11 am and are transmitted via Zoom.

Upcoming Talk

  • Programmatic Reinforcement Learning: why and how?
    Roman Kniazev (LaBRI, Université de Bordeaux)
    Friday, 24th January 2025, 11:00 (1Z71)
    Abstract:
    Reinforcement Learning has achieved remarkable success in the past decade, employing deep neural networks to represent policies. However, the interpretational opaqueness of these networks poses a challenge, making it difficult to comprehend and reason with the policies they generate. In response to this growing demand for interpretability and verifiability, the field of Programmatic Reinforcement Learning has emerged. The objective of this field is to learn policies in the form of programs.
    In this talk, I will provide an overview of the existing approaches to using programs as policies. In particular, I will focus on our rapid Jax-based implementation of a recently proposed algorithm for learning oblique decision trees, a machine learning model that stands out by being simultaneously a simple if-then-else program.

Recent Talks

Publications

A list of AI-related publications by LMF members can be found at the following link: https://hal.science/LMF-AI

Projects and Collaborations

  • ACTER: Analyse cognitive des émotions
  • DyLo-MPC: Dynamic Logics: Model Theory, Proof Theory and Computational Complexity
  • ETSHI: Efficient Test Strategies for SARS-CoV-2 in Healthcare Institutions
  • LeaRNNify: New Challenges for Recurrent Neural Networks and Grammatical Inference
  • SAIF: [S]afe [AI] through [F]ormal Methods
  • SINFIN: Méthodes formelles pour la modélisation, la spécification, la vérification et le développement de logiciels

Members

Permanent

Emeritus

PhD Students

Mariapia D'Urso

Nicolas Dumange

Associated

Zhuofan Xu