Description

Les systèmes d’IA ont de plus en plus d’influence sur la prise de décision dans des domaines critiques tels que la santé et le droit. Il est donc essentiel de garantir la transparence et la responsabilité. De nombreux modèles d’IA, en particulier ceux basés sur l’apprentissage automatique, fonctionnent comme des « boîtes noires », ce qui rend leur raisonnement difficile à interpréter et à vérifier. Les approches traditionnelles d’IA basées sur la logique ne parviennent souvent pas à saisir les nuances dont l’IA fait preuve face à l’incertitude et justifie ses conclusions.

Cette recherche propose la logique modale intuitionniste (IML) comme base pour les systèmes d’IA qui nécessitent des justifications explicites pour leurs décisions. L’IML étend la logique intuitionniste, qui exige que les déclarations soient prouvées de manière constructive plutôt que simplement supposées vraies ou fausses. Sa composante modale introduit des distinctions entre certitude et possibilité, permettant à l’IA de raisonner sur ce qu’elle sait définitivement et sur ce qui reste incertain. Cette approche est particulièrement utile dans les domaines où les décisions doivent être explicables et défendables juridiquement. Par exemple, dans le diagnostic médical, une IA ne doit confirmer une maladie que si elle dispose d’une preuve constructive, tandis que les cas incertains doivent être signalés pour une évaluation plus approfondie.

L'objectif de cette recherche est de fournir les fondements théoriques de preuve permettant de mettre en place un cadre de raisonnement formel de l'IA pour garantir que les décisions de l'IA sont explicables, vérifiables et juridiquement responsables.
En intégrant l'IML, ce travail cherche à combler le fossé entre la logique formelle et les applications de l'IA dans le monde réel, en offrant une méthode pour construire des systèmes d'IA fiables et responsables.

Compétences requises

Le candidat retenu devra être familier avec les fondements de la logique et de la théorie de la preuve, et avec les principes d'IA

Bibliographie

[ADS15] Ryuta Arisaka, Anupam Das, and Lutz Straßburger. On nested sequents for con-
structive modal logic. LMCS, 11(3:7), 2015.

[Avr96] Amon Avron. The method of hypersequents in the proof theory of propositional
non-classical logics. In Logic: from Foundations to Applications: European logic
colloquium. Oxford University Press, 06 1996.

[Brü09] Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical
Logic, 48(6):551–577, 2009.

[CMS16] Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular focused proof
systems for intuitionistic modal logics. In Delia Kesner and Brigitte Pientka, editors,
1st International Conference on Formal Structures for Computation and Deduction,
FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 16:1–
16:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.

[GKM+ 23] Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz
Straßburger. Intuitionistic S4 is decidable. In 38th Annual ACM/IEEE Symposium
2on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023,
pages 1–13. IEEE, 2023.

[MMS21] Sonia Marin, Marianela Morales, and Lutz Straßburger. A fully labelled proof system
for intuitionistic modal logics. J. Log. Comput., 31(3):998–1022, 2021.
[Neg05]Sara Negri. Proof analysis in modal logics. Journal of Philosophical Logic, 34:507–
544, 2005.

[Sim94] Alex Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD
thesis, University of Edinburgh, 1994.

[Str13] Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal log-
ics. In Frank Pfenning, editor, FoSSaCS’13, volume 7794 of LNCS, pages 209–224.
Springer, 2013.

Mots clés

calcules de preuve, logique modale, IA