Formal Methods for Artificial Intelligence

The team is concerned with several topics at the interface between formal methods and artificial intelligence:

Symbolic reasoning about knowledge in terms of logic has applications in planning, synthesis, or reasoning about the strategic behavior of intelligent agents. Prominent relevant logics are, e.g., description logics (logics for knowledge representation), strategy logics (to reason about the strategic behavior of agents), fuzzy logic, and dynamic logics (extensions of modal logic).

The goal of model learning is to infer a model from a black box, a system that can be accessed only in a very restricted manner. It has applications in the verification and testing of legacy software, or the extraction of structural information from ML components such as neural networks.

It is well known that deep neural networks can be fooled easily by introducing some noise in the inputs. And depending on the application, this is a safety and security risk. We are exploring in how far formal methods can be exploited to develop a sort of robust and verified AI and machine learning. Moreover, we are interested in explainable AI to justify why certain decisions of machine-learning components were taken.

Last, machine learning is not only an application domain of formal methods. It can also complement formal methods in applications like controller synthesis, especially in cyber-physical systems, autonomous cars, etc.

Members

Permanent

Emeritus

PhD Students

Projects

  • STIC AmSud – DyLo-MPC: Dynamic Logics: Model Theory, Proof Theory and Computational Complexity
  • IRP – SINFIN: Méthodes formelles pour la modélisation, la spécification, la vérification et le développement de logiciels
  • Égide/Procope – LeaRNNify: New Challenges for Recurrent Neural Networks and Grammatical Inference