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

  • How to manage a budget with ATL+
    Stéphane Demri (LMF, CNRS)
    Friday, 25th October 2024, 11:00 (room tba)
    Summary: We study ATL+ enriched with one resource (written ATL+(1)) extending ATL+ with the possibility to manage a budget. We propose a game-theoretic semantics via the introduction of two evaluation games so that the compositional semantics is captured by strategies in the games. We show that the model-checking problem for ATL+(1) is in PSpace and we identify fragments in PTime. By-products of our investigations include a simplified PSpsace decision procedure for resource-free ATL+ based on small strategy skeletons, the synthesis of constraints in ATL+(1) with parameters and a PSpace bound to solve a close energy game problem with one counter and objectives of temporal depth one. This is a joint work with Raine Ronnholm. Paper available at https://proceedings.kr.org/2023/19/.

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

Associated

Zhuofan Xu