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 in developing 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 for the identification of 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

  • Friday, 26th January 2024, 11:00 (room tba)
    First Steps Towards Taming Description Logics with Strings
    Stéphane Demri (LMF, CNRS)
    Abstract: We consider a description logic over a concrete domain with the strict prefix order over finite strings. Using an automata-based approach, we show that the concept satisfiability problem w.r.t. general TBoxes is ExpTime-complete for all finite alphabets. As far as we know, this is the first complexity result for an expressive description logic with a nontrivial concrete domain on strings. This is a joint work with Karin Quaas (Leipzig University). Paper available at: https://hal.science/hal-04212642

Recent Talks

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
  • SINFIN: Méthodes formelles pour la modélisation, la spécification, la vérification et le développement de logiciels
  • vrAI: FOrmal VeRification and AI (DigiCosme working group)

Members

Permanent

Emeritus

PhD Students

Zhuofan Xu

Associated