Sites Inria

English version

Équipe de recherche

Charlotte Renauld - 27/06/2016

Rencontre avec l'équipe DEDUCTEAM

L’équipe DEDUCTEAM a rejoint le centre Inria Saclay – Île-de-France au 1er janvier 2016. Cette équipe en pleine transformation travaille sur les notions de preuve et de déduction. Rencontre avec Gilles Dowek, responsable de l’équipe DEDUCTEAM dans ses bureaux à l’ENS Cachan.

L'Équipe DEDUCTEAM

L’équipe DEDUCTEAM est composée de deux chercheurs permanents, Frédéric Blanqui et Gilles Dowek, responsable de l’équipe, qui s’attachent à développer des réseaux de coopération avec plusieurs établissements, notamment l’École des Mines, l’ENSIIE et l’Université de Montpellier, dans le but de maintenir des liens scientifiques autour d’intérêts communs. 

Le nom « Deducteam » a trois origines : le mot « team », le mot « déduction », et le nom provenant de l’esperanto « Dedukti », l’outil principal développé par les membres de l’équipe depuis 5 ans.

Le domaine de la preuve et de la déduction

Plusieurs équipes du centre Inria Saclay – Île-de-France travaillent sur les notions de preuve et de déduction : SPECFUN, TOCCATA, PARSIFAL et DEDUCTEAM.

En informatique, ces notions intéressent les chercheurs à deux titres :

  • Tout d’abord, il s’agit d’expliquer à un ordinateur pourquoi quelque chose est vrai afin que la machine puisse chercher d'éventuelles erreurs dans la démonstration, que l'on ne peut pas toujours vérifier « à la main », par exemple parce qu'elles est trop longues.
  • Plus fondamentalement, la notion de preuve doit son importance en informatique au fait que les ordinateurs sont des machines à énoncer des vérités. Par exemple, on pourrait attendre d’un système d’aide au diagnostic médical qu’il fournisse non seulement le nom de la maladie lorsque l’on entre les symptômes du patient, mais également le raisonnement qui l’a mené à nous donner le nom de la maladie et le traitement adéquat. 

La sûreté au cœur de la recherche

Une autre motivation pour s'intéresser à la notion de preuve est que c'est un outil essentiel pour assurer la sûreté de fonctionnement des programmes informatiques. Lorsque l’on construit un programme, on utilise des démonstrations qui doivent être correctes et vérifiées pour éviter les bugs. Cette question de la sûreté est essentielle dans au moins trois domaines :

  • Le transport : « Les êtres humains sont moins bons que les ordinateurs pour effectuer des tâches très monotones comme conduire sur l’autoroute. Dans les 10 prochaines années, la recherche tend à ce que l’ordinateur prenne le relais du conducteur sur l’autoroute par exemple. », nous explique Gilles Dowek.
  • La santé : « On s’aperçoit que les robots font de meilleurs chirurgiens que les chirurgiens. Par exemple, pour une opération à cœur ouvert, pour que le chirurgien atteigne le coeur il faut casser la cage thoracique. Aujourd’hui, des robots arrivent à opérer le cœur sans blesser le patient par ailleurs. »
  • Et l’énergie (en particulier nucléaire) pour entre autres contribuer à la sécurité des équipements.

Dans tous ces domaines, il s’agit de développer des systèmes de vérification qui évitent les bugs informatiques et par conséquent les accidents aux conséquences gravissimes.

Un système de preuve universel et interopérable : Dedukti

Il existe différents systèmes de preuve qui ont été développés dans le monde mais qui ne sont pas interopérables : un système ne reconnait pas les preuves développées dans un autre système. C’est le problème auquel DEDUCTEAM s’est attaqué en créant il y a cinq ans un système de preuve universel qui permet de passer d’un langage à l’autre : Dedukti. Ce nom qui veut dire « déduire » en esperanto a été choisi pour illustrer cet objectif d’universalité à atteindre.

La principale réalisation de l’équipe est d’avoir créé un écosystème composé d’un système universel (Dedukti) et de cinq systèmes capables de traduire les preuves issues des autres systèmes créés par d’autres équipes dans le monde.

Une équipe à la croisée des chemins

Aujourd’hui, DEDUCTEAM travaille sur deux nouveaux objectifs :

  • Permettre la réutilisabilité des démonstrations, c’est-à-dire, être capable à l’intérieur de Dedukti de comprendre comment transférer une preuve d’un langage à un autre. C’est ce que l’on appelle l’interopérabilité des systèmes : le fait qu’ils puissent échanger des informations.
  • Créer une « Bibliothèque de Babel » : une fois que l’on est capable de faire cette analyse des démonstrations, il faut pouvoir les ranger dans « une bibliothèque » hétérogène ou « une encyclopédie » dans laquelle les différents systèmes pourraient aller puiser les éléments dont ils ont besoin.

Mots-clés : Gilles Dowek Deducteam Preuve Déduction

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !