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
- 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)
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