Alain Finkel : de l’informatique théorique aux sciences cognitives

Quels sont vos travaux de recherche en informatique ?

Alain Finkel : Cette nomination à l’IUF va me permettre de me consacrer plus amplement à la recherche en informatique. En effet, depuis 35 ans, je suis enseignant-chercheur dans le domaine de la vérification de systèmes. En 1986, j’ai élaboré la théorie des systèmes bien structurés (c’est-à-dire des systèmes à ensembles infinis d’états possédant deux propriétés : la monotonie des transitions et l’existence d’un bel ordre sur l’ensemble des états). Cette théorie, qui continue à être utilisée et développée encore aujourd’hui, propose plusieurs algorithmes de vérification de modèles. L’un de ces algorithmes vérifie que le programme termine. Un autre algorithme vérifie que l’espace utilisé par le programme est fini. Un troisième algorithme vérifie que l’ensemble de tous les états accessibles du système ne contient pas d’erreurs. En termes d’applications, cette théorie est largement utilisée pour vérifier des programmes informatiques allant des protocoles de communication ou de gestion des mémoires aux systèmes répartis et distribués. Prenons l’exemple des transports : le coût des voitures, trains, avions, etc. est de plus en plus constitué par l’informatique. Les commandes relèvent de moins en moins de la mécanique et de l’hydraulique et sont remplacées par l’automatisme et des signaux informatiques. Les algorithmes doivent donc aujourd’hui vérifier qu’une porte de train ne puisse s’ouvrir quand ce dernier est encore en mouvement ou qu’un système informatique de freinage d’une voiture est efficace. La théorie des systèmes bien structurés a été utilisée et améliorée au cours des années.

Pouvez-vous nous en dire plus sur ces nouveaux projets de recherche ?

A. F. : Un 2^ème point de mes travaux en informatique que je souhaite développer dans les cinq ans à venir est un outil de vérification pour les modèles de réseaux de Petri. Un réseau de Petri est un modèle mathématique avec un ensemble fini de places contenant un ensemble fini de jetons et pour lesquelles, des règles de franchissement définissent les manières dont les jetons sont transférés, créés ou détruits de places en places. À ce jour, il n’existe aucun outil implémentant un algorithme vérifiant la propriété d’accessibilité d’un état initial à un état final dans un réseau de Petri. La difficulté est qu’il peut y avoir un très grand nombre, voire une infinité, de possibilités de passer d’un état initial à un état final. Or, pour qu’un algorithme fonctionne, il faut déjà qu’il termine. Bien sûr, il existe des outils pour les réseaux bornés qui ne contiennent qu’un nombre fini d’états accessibles, mais la vérification est bien plus complexe pour les systèmes qui possèdent une infinité d’états accessibles.

Vous êtes également enseignant en sciences cognitives : quels sont les liens avec les sciences informatiques ? Qu’est-ce qui vous a amené à avoir cette double vocation ?

A. F. : L’informatique m’a attiré car elle proposait un modèle simplifié de la pensée humaine et de la communication. Je ne suis pas le premier car les fondateurs de l’informatique moderne dans les années 1930 (Turing, Church) et de la logique avaient aussi à cœur de mieux comprendre l’esprit humain via des modèles simplifiés. Et on pourrait facilement remonter plusieurs siècles et trouver des philosophes passionnés par les algorithmes : les philosophes Descartes, Pascal et Leibniz étaient évidemment intéressés par la compréhension et la formalisation de la pensée et ils ont construit des machines à calculer. En parallèle de ma maîtrise de mathématiques et de ma thèse en informatique, j’ai donc commencé une licence en sciences de l’éducation et une licence de psychologie car je voulais aussi apprendre et comprendre les théories de l’esprit produites par les pédagogues et les psychologues.

Et je vois des similitudes au moins en terme de buts entre les modèles de programme et les modèles de la pensée humaine. Aujourd’hui le deep learning en est une sorte d’émanation victorieuse. Je suis d’ailleurs en train d’étudier l’utilisation de certains outils d’IA pour vérifier des programmes.

Quand j’ai été nommé professeur à l’ENS Cachan (aujourd’hui l’ENS Paris-Saclay), ma priorité a été de fonder un laboratoire de recherche en informatique et un département d’enseignement de l’informatique. J’ai donc mis un peu de côté mes intérêts de recherche cognitifs. Quand l’informatique a été bien établie dans les années 2000, grâce au collectif de collègues recrutés à l’ENS Cachan, j’ai pu consacrer un peu de temps à encadrer des thèses en sciences cognitives et à former les étudiants aux sciences cognitives appliquées à l’enseignement et à la pédagogie. Par la suite, ces cours de pédagogie furent les prémices d’une formation pédagogique et cognitive appelée ACTA (Analyse Cognitive des Techniques d’Apprentissage), créée en 2006, à destination des enseignants, enseignants-chercheurs, doctorants et normaliens.

Dans le cadre de mes différents projets, il y a donc quelques relations entre l’informatique de la vérification de modèles et les modèles de la pensée que j’essaie d’élaborer.

Cette nomination à l’IUF va donc me permettre d’écrire des ouvrages en analyse cognitive, pédagogie et psychologie : comment les étudiants pensent, apprennent, mémorisent, se motivent, comprennent, etc. Je compte proposer des méthodologies pour comprendre comment l’esprit fonctionne par un questionnement cognitif que j’ai mis au point.