Spécifications, contraintes et preuves

La problématique considérée dans ce thème concerne la formalisation de la géométrie pour démontrer des théorèmes, construire des figures ou, plus généralement, des scènes géométriques, et certifier des algorithmes en géométrie.

Plus précisément, nous nous intéressons à la définition formelle d'univers géométriques, la preuve de propriétés, la production automatique d'objets géométriques définis par une spécification exprimée dans cet univers géométrique et la dérivation d'algorithmes géométriques certifiés corrects. Nous nous penchons sur des méthodes informatiques permettant d'assister les preuves, de garantir la correction et la faisabilité et, dans la mesure du possible, d'assurer automatiquement certaines tâches notamment à travers l'étude de tactiques Coq ou, dans un autre registre, la résolution de contraintes géométriques. Les retombées attendues concernent des domaines tels que la modélisation géométrique, l'algorithmique géométrique, la géométrie pure, l'enseignement des mathématiques et la planification assistée d'opérations chirurgicales percutanées ou assimilées.

Cela s'est traduit lors de ces dernières années par des activités de recherche dans quatre directions légèrement différentes mais participant du même esprit :

• Formalisation de la géométrie et preuves de théorèmes géométriques ;
• Spécification et preuves d'algorithmes géométriques en utilisant des cartes combinatoires ;
• Spécification de figures et résolution de contraintes ;
• Formalisation et planification d'opérations percutanées dans le cas de l'ablation de tumeurs hépatiques et d'intervention radiologiques.

Participants permanents

• Deux professeurs: Jean-François Dufourd et Pascal Schreck
• Quatre maîtres de conférences: Caroline Essert, Nicolas Magaud, Pascal Mathis, Julien Narboux

Autres participants

• 1 Chercheur associé: Gabriel BRAUN (MC UFR LSHA, 09/2009-)
• 1 Maître de conférence en délégation CNRS: Laurent FUCHS (MC Poitiers, 09/2010-09/2011)
• 3 Post-doctorants: Claire BAEGERT (ATER, 01/2010-08/2010), Christophe BRUN (ATER, 01/2011-08/2011), Simon THIERRY (ATER, 10/2010-08/2011)
• 1 Doctorants: Rémi IMBACH (Ministère, 10/2010-)
• 3 Anciens doctorants: Claire BAEGERT (Région Alsace-IRCAD, 10/2005-12/2009), Christophe BRUN (Ministère, 12/2007-12/2010), Simon THIERRY (Ministère, 10/2006-09/2010).

Formalisation et preuves de théorèmes en géométrie

Nous nous intéressons ici à la preuve, automatique ou assistée par ordinateur, en géométrie. Parmi les directions de recherche classiques, comme, par exemple, les axiomatisations ad hoc, la formalisation des fondements, les preuves algébriques ou les preuves combinatoires, nous nous sommes principalement penchés sur les questions de formalisation et d'axiomatisation de divers modèles géométriques.

C'est ainsi que pour avoir des solveurs de contraintes géométriques robustes (voir section suivante), nous nous sommes tout d'abord intéressés à des géométries très simples comme la géométrie projective d'incidence. Nous nous sommes tout d'abord placés dans un cadre axiomatique approprié pour concevoir des prouveurs automatiques basés sur des propriétés d'incidence fondamentales comme les configurations de Desargues, de Pappus, de l'hexagramme de Pascal (ou hexamys) ou encore les structures de matroïdes. Nous avons collaboré avec D. Michelucci, professeur en informatique à l'Université de Bourgogne pour mettre au point divers prototypes permettant de faire des preuves combinatoires, c'est-à-dire sans faire aucun calcul numérique, d'alignements ou de coïncidences automatiquement.

Théorème de Desargues

Nous avons ensuite rapidement été amenés à travailler sur les fondements des géométries d'incidence. Ce qui a constitué un volet du projet ANR blanc GALAPAGOS (2008-2011) sur la preuve assistée en géométrie. Dans ce cadre, nous avons spécifié et implanté en Coq diverses axiomatiques pour étudier des espaces projectifs de plus en plus riches (voir 4-MNS08). Parmi les résultats notables que nous avons obtenus, il faut citer une preuve complètement formalisée en Coq, du théorème de Desargues en utilisant uniquement la théorie des matroïdes à travers la notion de fonction de rang à laquelle nous avons ajouté des propriétés liées à la dimension (la propriété de Desargues ne devient vraie en géométrie d'incidence qu'à partir de la dimension 3) 4-MNS09. Nous travaillons actuellement sur d'autres théorèmes en dimension 3, comme le théorème de Beltrami, avec pour objectif la conception d'un logiciel de preuve en géométrie d'incidence aussi complet que possible.

En ce qui concerne l'automatisation des preuves, Julien Narboux a réalisé en Coq la première formalisation d'une méthode de démonstration automatique en géométrie (la méthode des aires), cela a conduit en collaboration avec Pedro Quaresma et Predrag Janicic à un article de référence sur la méthode (2-JNQ10). Ce développement a été intégré à un environnement de preuve interactive au sein du logiciel de géométrie dynamique GeoGebra (4-PBN11).

Plus fondamentalement encore, nous travaillons en collaboration avec Laurent Fuchs, maître de conférences en informatique à l'Université de Poitiers, à la formalisation en Coq d’un modèle discret du continu : la droite d'Hartong-Reeb. Ces travaux en cours pourront donner lieu à une implantation effective du continu sur ordinateur 7-MCF10a. A plus long terme, nous envisageons de prouver formellement les résultats obtenus sur l'arithmétisation des fonctions et la connectivité des ellipses.

Enfin, dans le but plus pragmatique d'avoir un prouveur puissant en géométrie euclidienne, nous avons commencé des travaux concernant la certification en Coq de méthodes algébriques basées sur la preuve de l'appartenance d'un polynôme à un idéal et le Nullstellensatz d'Hilbert. Deux directions classiques ont commencé à être étudiées : la méthode de Ritt-Wu et une méthode utilisant les bases de Gröbner.

Spécification, preuves d'algorithmes et implantation

Cette recherche reconsidère la modélisation et l'algorithmique géométriques à travers des spécifications formelles et des preuves assistées par ordinateur. Elle s'appuie d'une part sur la modélisation géométrique à base topologique des subdivisions d'espaces par des hypercartes combinatoires, et d'autre part sur le Calcul des constructions inductives et le système Coq de l'INRIA. Cette manière d'aborder les problèmes n'a pas d'équivalent au monde. Ce travail est l'un des volets du projet ANR Blanc GALAPAGOS (2008-2011) sur la preuve assistée en géométrie. Par l'aspect topologie combinatoire, il est étroitement lié au thème "Modélisation et acquisitions" de l'équipe IGG.

Théorème de Jordan discret

Après tout un travail avec des spécifications algébriques, nous avons, depuis la fin des années 90, formalisé les hypercartes et leurs dérivés (cartes et cartes généralisées) et construit une bibliothèque Coq sur ces structures. Des preuves formelles ont été produites pour de grands résultats de topologie combinatoire : théorème de classification des surfaces, théorème du genre, formule d'Euler-Poincaré 2-Duf08a.

Segmentation - A gauche : image initiale ; A droite : image segmentée

Rotation d'arête décomposée par split et merge

Durant le présent contrat quadriennal, nous avons énoncé et prouvé un théorème de Jordan discret, donnant un critère de déconnexion des hypercartes utile pour prouver des algorithmes sur les hypercartes 4-Duf08b 2-Duf09. Nous avons proposé un algorithme fonctionnel de segmentation d'images 2D faisant un pattern-matching sur la structure inductive des cartes combinatoires décrivant les images. Nous en avons prouvé la correction en Coq et avons pu en dériver un programme impératif (en C) efficace, qui a été expérimenté sur des images couleur en vraie grandeur.(Travail de J.-F. Dufourd 2-Duf07).

Nous avons aussi étudié plusieurs problèmes liés à l'algorithmique géométrique. Ainsi, nous avons travaillé sur les algorithmes de construction d'enveloppe convexe. Deux versions en ont été étudiées et prouvées correctes en Coq. La première, qui travaille par induction structurelle, repose sur des idées semblables à la segmentation évoquée précédemment. La seconde, qui repose sur une induction noethérienne, simule un algorithme traditionnel de construction incrémentale. Des programmes en ont été automatiquement extraits en Ocaml, et, de la seconde version a été dérivé un programme en C++, qui a été intégré à la plateforme CGoGn d'IGG. (Travail de thèse de C. Brun, encadré par J.-F. Dufourd et N. Magaud 2-BDM11a 7-BDM11b).

Un gros travail a été effectué sur la formalisation des subdivisions de surfaces, avec les opérations merge et split pour fusionner et éclater des cellules d'hypercartes. Il a été particularisé aux triangulations avec la définition de l'opération classique de rotation (ou flip) d'arêtes. Ceci nous a conduit à la première formalisation et preuve assistée en Coq d'un algorithme de construction d'une triangulation de Delaunay. Celle-ci travaille par une suite de rotations jusqu'à ce que toutes les arêtes soient valides par rapport à un critère de cercle de Delaunay. (Travail de J.-F. Dufourd et Y. Bertot, directeur de l'équipe Marelle de l'INRIA-Sophia 4-DB10).

Spécification et résolution de contraintes géométriques

La question de la spécification d'objet par la donnée de quelques unes de ses dimensions (cotes fonctionnelles ou cotes de fabrication) fait partie des questions importantes dans le domaine des dessins et conceptions assistés par ordinateur (CAO). Elle est étroitement liée à la production d'un dessin à l'échelle répondant au système de cotes posé par l'utilisateur. On regroupe habituellement ces questions, et d'autres, dans la problématique de la résolution de contraintes géométriques. Depuis les années 80, plusieurs méthodes ont été développées en vue de résoudre des systèmes de contraintes géométriques. On peut grossièrement les regrouper en trois familles: les méthodes numériques qui résolvent de manière itérative des systèmes d'équation, les méthodes à base de graphe pour faire de la planification et les méthodes à base de système de connaissances pour résoudre constructivement les systèmes de contraintes (Cf. les constructions à la règle et au compas). Les méthodes de la dernière famille donnent lieu à une formalisation de la géométrie qui fait la spécificité de notre équipe. Il existe aussi des méthodes algébriques formelles utilisant, par exemple, des bases de Gröbner, mais, habituellement, leur complexité les disqualifie dans le cadre de la CAO.

Deux caractéristiques ont guidé les travaux des spécialistes du domaine ces dernières années :

• la grande taille et le caractère creux des systèmes de contraintes
• l'invariance par déplacement (ou plus généralement par des groupes de transformations)

Le premier point a poussé les équipes à s'intéresser à la décomposition des systèmes de contraintes et le deuxième à tenir compte de l'invariance par déplacement lors de ces décompositions. On obtient alors des méthodes particulières qui ne s'apparentent pas forcément aux méthodes de flux rencontrées dans les méthodes de décomposition des systèmes d'équations.

Ces questions d'invariance et de décomposition ont été théorisées par notre équipe (voir 2-MT10), ce qui a permis de mettre au point des méthodes prenant en compte plusieurs groupes et dont l'implantation s'est faite sous la forme d'un système multi-agents permettant de regrouper plusieurs solveurs de natures différentes. Une autre manière plus probabiliste de voir les choses nous a conduit à proposer une méthode incrémentale pour décomposer les systèmes de contraintes (travail réalisé en collaboration avec Dominique Michelucci, 4-MSTF10).

Le problème de la décomposition des systèmes de contraintes géométriques implique souvent que les sous-systèmes isolés soient bien-contraints modulo un groupe de transformations donné. En effet, les solveurs classiques ne gèrent habituellement que les systèmes avec un nombre fini de solutions, éventuellement après avoir quotienté l'espace des solutions par une relation liée à l'action d'un groupe de transformations. Malheureusement, de nombreux exemples simples montrent qu'en dimension 3, cette notion de décomposition n'est plus intéressante : la plupart des polyèdres sont génériquement rigides et indécomposables de ce point de vue. C'est pourquoi dans la thèse d'Arnaud Fabre, nous nous sommes intéressés à une notion de quasi-décomposabilité dans laquelle on autorise dans une première étape la modification du système de contraintes. Les contraintes oubliées dans cette étape sont rattrapées ensuite en utilisant une méthode numérique (voir 4-FS07 et 4-FS08).

Naturellement, suivre cette approche conduit à considérer des systèmes sous-contraints, même en considérant les groupes de transformations classiques (5-TSMF08 et 4-TMS07). Ce fut naturellement un des volets de la thèse de Simon Thierry (8-Thie10), dont l'objet a été d'étudier les questions de sous-constriction dans les systèmes de contraintes. Une approche originale a d'ailleurs été implantée par Simon Thierry qui peut résoudre (en un certain sens) des systèmes de contraintes sous ou même sur-contraints (voir 4-Thie11).

Formalisation et planification d'opérations percutanées

Dans ce travail nous proposons une approche originale pour l'assistance à la planification avec automatisation du positionnement d'un outil chirurgical. Notre méthode permet d'élaborer une stratégie optimale d'intervention, spécifique au patient et au type d'opération concerné, grâce à un calcul automatique qui se base à la fois sur l'expertise du domaine et sur des données préopératoires.

Pour atteindre cet objectif, nous avons mis en œuvre des approches issues de la modélisation déclarative et de la résolution de contraintes géométriques pour calculer automatiquement des trajectoires optimales d'outils chirurgicaux rectilignes rigides. Le calcul de trajectoire se fait en plusieurs étapes. Tout d'abord, l'expertise du praticien sur un type d'intervention donné est retranscrite sous forme d'équations mathématiques (égalités, fonctions de coût). Puis ces équations sont formalisées en contraintes géométriques, écrites sous la forme de termes combinant opérateurs géométriques et arithmétiques, et données issues des images médicales (IRM, CT). Un premier calcul permet de résoudre les contraintes géométriques dites "strictes" (booléennes) pour donner l'espace des solutions. Enfin, un deuxième calcul permet de résoudre les contraintes géométriques dites "souples" (numériques), grâce à une optimisation numérique, pour donner la solution optimale.

Nous avons testé nos approches sur 2 types d'interventions : l'ablation de tumeurs hépatiques par radiofréquence (hyperthermie) en collaboration avec le Pr. Gangi du service de radiologie interventionnelle de l'Hôpital Civil de Strasbourg, et l'implantation d'électrodes de stimulation cérébrale profonde en collaboration avec le Dr. Haegelen du service de neurochirurgie du CHU de Rennes Pontchaillou.

Le travail de thèse de Claire Baegert a porté sur ces travaux 8-Baeg09. De nombreuses publications ont porté sur ces thèmes, concernant la radiofréquence 4-EBS09, 2-BESS07, 4-BESS07, 4-BESS07b, 4-BESS07c et la stimulation cérébrale profonde 4-EHJ10. Ces travaux ont également donné lieu à une collaboration avec le DKFZ de Heidelberg sur l'accélération des calculs d'obstacles aux trajectoires par GPU 5-ESFR10, 2-SESR11.

Ces travaux ont donné lieu au projet ANR blanc ACouStiC, qui a démarré en janvier 2011 pour une durée de 4 ans, et dont IGG est partenaire. Ce thème de recherche s'insère également dans le cadre de l'IHU Mix-Surg.

Perspectives

Formalisation et preuves de théorèmes en géométrie

Nous souhaitons étudier d'autres théorèmes fondamentaux en géométrie d'incidence comme le théorème de Beltrami et appliquer ces recherches à la création d'un prouveur certifié pour la géométrie de l'incidence.

Les travaux sur la génération automatique de preuve vont être renforcés par la formalisation de méthodes algébriques comme la méthode de Wu. Du point de vue de l'ingénierie de la preuve nous allons utiliser une méthode à bases de certificats. Cette thématique rejoint une des thématiques de l'équipe INRIA Camus à laquelle Julien Narboux et Nicolas Magaud participent et qui s'intéresse à la preuve formelle d'algorithme de compilation parallèle et d'optimisation de programmes à l'aide de modèles dits polyédriques en utilisant aussi une approche à base de certificats.

Enfin, nous allons combiner nos travaux concernant la preuve automatique de théorèmes et la résolution de contraintes géométriques en formalisant au sein du système Coq ces différentes concepts. L'objectif est d'une part de générer des algorithmes de résolution de contraintes certifiés et d'autre part d'élargir les champs d'application des méthodes de démonstration automatique en géométrie (car les méthodes de démonstration automatique existante supposent l'existence d'une construction géométrique).

Spécification, preuves d'algorithmes et implantation

Le travail sur la formalisation des structures combinatoires topologiques sera consolidé et amplifié. La bibliothèque d'hypercartes sera révisée et étendue en dimension n pour décrire et manipuler des subdivisions d'espace nD. Des liens seront établis avec les algorithmes de calcul des groupes d'homologie des variétés de dimension n.

L'expérimentation en preuves d'algorithmes géométriques sera poursuivie. L'accent sera mis sur les algorithmes de triangulation de Delaunay et de Voronoï en dimension 3, qui sont toujours des challenges, notamment en présence de contraintes. La question des approximations numériques sera également abordée. Jusqu'ici, elle a été évacuée de nos travaux au profit de calculs exacts dans les réels. Cette position devra être révisée, en examinant différentes hypothèses de travail : calcul exacts sur des rationnels, calculs approchés par intervalles, géométrie discrète, etc.

Enfin, le raffinement de nos structures abstraites d'hypercartes en structures concrètes en mémoire devra être étudié. Le passage de nos algorithmes abstraits en programmes impératifs concrets avec pointeurs sera étudié, avec la preuve de conservation de la correction. Un travail préliminaire sur les structures linéaires et cycliques a déjà permis d'obtenir des résultats prometteurs.

Spécification et résolution de contraintes géométriques

Afin de résoudre des systèmes de contraintes géométriques, nous avons toujours privilégié l'emploi de méthodes géométriques. Outre leur capacité a fournir toutes les solutions, elles offrent un diagnostic en cas d'échec en indiquant les contraintes en cause dans l'arrêt de la résolution. Cependant certains cas d'école en 2D et de nombreux problèmes concrets en 3D résistent à ces méthodes.

Nous étudions actuellement la transformation d'un système S en un système S' résoluble géométriquement. Le passage des solutions de S' à celle de S s'effectue numériquement. Ce travail en cours s'attaque à deux problèmes. Le premier porte sur le lien entre la transformation d'un système et sa décomposition, tout cela afin de faciliter la résolution numérique. Le second concerne l'adaptation de méthodes numériques pour s'appuyer sur toutes les informations géométriques disponibles (l'esquisse fournie par l'utilisateur, le plan de construction produit par la résolution).

A côté de ce travail qui tente d'allier les méthodes numériques utilisées dans l'industrie et les méthodes géométriques plus au goût du monde académique, se poursuit un important travail de réalisation d'une plateforme de solveurs utilisée et enrichie par tous les intervenants dans ce domaine, aussi bien les enseignants-chercheurs d’IGG que les stagiaires des formations. Ce travail s'appuie sur un langage de description de systèmes de contraintes, aussi bien leur syntaxe que leur sémantique, initié il y a quelques années par l'équipe.

Formalisation et planification d'opérations percutanées

Concernant la planification d'opérations chirurgicales, dans le cadre entre autres du projet ANR blanc ACouStiC, nous allons entamer une extension du domaine des solutions possibles, en étudiant les trajectoires courbes et/ou multiples, ainsi que les trajectoires volumiques. Cela nous permettra d'étendre le champ des applications à des outils chirurgicaux déformables, insérés dans des tissus également déformables, ou encore à des outils multiples (par exemple la cryoablation de tumeurs du foie), ou enfin à des volumes d'accès par exemple pour la craniotomie dans le cadre d'exérèse de lésions cérébrales. Nous allons également travailler à la navigation contrainte dans l'espace des solutions, afin de restreindre la modification de la trajectoire proposée à un espace des solutions possibles et/ou raisonnables. Pour cela, le lien sera fait avec l'axe "Visualisation et interactions" et notamment le thème de recherche sur les interfaces à retour d'effort.