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
- Empreinte environnementale de l'IA : quelles méthodes et résultats ?
Anne-Laure Ligozat (LISN & ENSIIE)
Friday, 28th March 2025, 15:30 (1Z56)
Résumé:
L'empreinte environnementale du numérique et en particulier de l'IA fait l'objet de nombreux questionnements. En plus des impacts liés au cycle de vie des équipements informatiques impliqués dans un service d'IA, l'IA a également des impacts sur d'autres secteurs, qu'ils soient positifs, via par exemple l'optimisation de la consommation énergétique de bâtiments ou négatifs, via par exemple l'incitation à l'achat de produits non indispensables.
Dans cet exposé, je présenterai les méthodologies de calcul d'empreinte environnementale que j'ai développées, fondées notamment sur l'analyse du cycle de vie.
Recent Talks
- Recent advances in exact algorithms for the Multiagent Path Finding problem
Foivos Fioravantes (Czech Technical University in Prague)
Friday, 24th March 2025, 11:00 (online)
- Programmatic Reinforcement Learning: why and how?
Roman Kniazev (LaBRI, Université de Bordeaux)
Friday, 24th January 2025, 11:00 (1Z71)
- How to manage a budget with ATL+
Stéphane Demri (LMF, CNRS)
Friday, 25th October 2024, 11:00 (room 1Z61)
Paper available at: https://proceedings.kr.org/2023/19/ - Statistical Language Modeling: From N-grams to Transformers
Gustave Cortal (LMF)
Friday, 31st May 2024, 11:00 (room 1Z18)
Recorded talk: https://www.youtube.com/watch?v=PenKM-gZX_4
Slides: https://gustavecortal.com/data/Gustave_Cortal_Tutorial_on_Language_Models.pdf - First Steps Towards Taming Description Logics with Strings
Stéphane Demri (LMF, CNRS)
Friday, 26th January 2024, 11:00 (room 1Z71)
Paper available at: https://hal.science/hal-04212642 - An approach for inferring geometric expressions in topology-based modeling
Romain Pascual (MICS, CentraleSupélec, Université Paris-Saclay)
Friday, 6th October 2023, 11:00 (room 1Z56)
Slides: https://romainpascual.fr/talk/fmai2023/FMAI2023_slides.pdf - Updating Knowing How
Raul Fervari (Universidad Nacional de Córdoba / CONICET; Guangdong Technion - Israel Institute of Technology)
Friday, 29th September 2023, 11:00 (room 1Z56)
Slides: https://cs.famaf.unc.edu.ar/~rfervari/files/talks/2023-lmf.pdf - Autonomous systems in the intersection of formal methods, learning, and control
Ufuk Topcu (The University of Texas at Austin)
Friday, 23rd June 2023, 14:00 (room 1Z18) - Towards the Formal Verification of Neural Networks in Isabelle/HOL
Achim Brucker (Chair of Cybersecurity, University of Exeter, UK)
Friday, 26th May 2023, 11:00 (room 1Z56)
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
Associated
Zhuofan Xu