Pôle Interactions Formal Methods for Artificial Intelligence

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

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.

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

Friday, 15th December 2023, 11:00 (room 1Z56)
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

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)

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)

Zhuofan Xu