SCIENCE. Connaissez-vous cette discipline entre mathématiques et informatique qui révolutionne notre quotidien

Jusqu’au 6 juillet se déroule à Nancy un événement international de recherche avec des experts mondiaux de la logique et du raisonnement automatique. L’occasion d’expliquer cette discipline entre mathématiques et informatique.

C’est un événement scientifique international, organisé par des scientifiques de l'INRIA et de l'Université de Lorraine, qui se déroule jusqu’au 6 juillet à Nancy. Les experts mondiaux en logique et raisonnement automatique sont présents à l'Institut des sciences du Digital, Management Cognition (IDMC).

L’occasion de s’intéresser à un domaine de recherche passionnant qui a des applications concrètes au quotidien dans nos vies. Nous avons posé la question à Stephan Merz, directeur de recherche INRIA et responsable de l'équipe Veridis.

Comment définir cette discipline ?

C’est une discipline entre mathématique et informatique. "Elle permet des outils essentiels pour résoudre des problèmes complexes de manière méthodique et rigoureuse", précise Stephan Merz.
Le raisonnement automatisé est le domaine de l'informatique qui tente de fournir des garanties sur ce qu'un système ou un programme fera ou ne fera jamais. Cette assurance est basée sur des preuves mathématiques.
Pour résoudre des problèmes logiques en calcul, mathématiques ou en géométrie, on utilise des théorèmes et des déductions, donc des stratégies logiques. Le raisonnement automatisé utilise des ordinateurs, qui utilisent les mêmes outils pour résoudre des problèmes complexes.

Des applications concrètes

La logique et le raisonnement automatique ont des applications variées dans différents domaines. "On imagine aisément, dans le domaine de l’aviation ou des trains, la nécessité de certification avant la mise en service des logiciels. Il est important de garantir certaines propriétés de corrections, par exemple que deux trains n'occupent jamais un même tronçon de voie, que le métro s’arrête en face des portiques, ou que deux avions gardent toujours une distance minimale. Au niveau le plus exigeant de ces certifications, il est recommandé d’utiliser ces techniques de preuves formelles pour garantir ces propriétés. Nous avons besoin de ces techniques très sophistiquées et automatisées pour ces systèmes critiques", détaille le directeur de recherche INRIA.

Les mêmes techniques sont utilisées dans les systèmes à forts enjeux financiers, par exemple dans le système de stockage et de traitement en ligne, le cloud. Les entreprises ont besoin de garantir la disponibilité de leurs services, ce qui est également utile pour les systèmes bancaires.

Dans la programmation, la logique est utilisée pour écrire des algorithmes et des programmes informatiques. Le raisonnement automatique permet de vérifier la validité des programmes. Il pourrait être utilisé dans le cadre de la voiture autonome pour garantir les systèmes de sécurité contrôlant l’évitement. 

Lien avec le monde industriel

Un nombre croissant d'entreprises développant du logiciel font appel à des spécialistes en méthodes formelles pour vérifier par ordinateur, notamment grâce à des techniques de raisonnement automatique, le bon fonctionnement de composants informatiques critiques. La raison : une quelconque anomalie pourrait entraîner des conséquences dramatiques.

"Certains experts en déduction automatique travaillent pour les GAFAM ou pour les agences spatiales NASA ou ESA", raconte Stephan Merz.

La crème des experts est à Nancy

Cette année 2024, la ville de Nancy a été sélectionnée pour accueillir cet événement international. Il est organisé par des scientifiques du centre Inria et de l'Université de Lorraine. Les équipes de recherche de l'Université de Lorraine et du centre Inria sont à la pointe des travaux scientifiques menés dans ce domaine.

L'organisation d'une telle conférence est déterminante pour continuer de faire de Nancy une place forte en méthodes formelles, en vérification de systèmes complexes et en raisonnement automatique. 

Des ateliers et des conférences sont organisés jusqu’au 6 juillet à l'Institut des sciences du Digital, Management Cognition (IDMC) à Nancy.