Spécifications, Contraintes et Preuves en Géométrie

Objectifs / Challenges

La problématique de ce thème est centrée sur la question de la preuve et de la certification en géométrie et de ses applications en informatique. En amont, cela implique de spécifier formellement la théorie dans laquelle va se dérouler la preuve. Le logiciel Coq permet à la fois d'écrire de telles spécifications, mais aussi de faire des preuves en se faisant aider par l'ordinateur. Nous menons à la fois des recherches sur les fondements de la géométrie et sur l'application de prouveurs/solveurs dans les domaines de l'enseignement, de la CAO et de la planification d'opérations chirurgicales percutanées. L'objectif principal de nos travaux consiste à se rapprocher de l'utilisateur en lui fournissant des outils pour spécifier formellement un problème géométrique et pour faciliter la construction d'une preuve en utilisant notamment des prouveurs et des solveurs automatiques.

Participants

Deux professeurs : Pascal Schreck, Jean-François Dufourd (professeur émérite)
Cinq maîtres de conférences : Gabriel Braun, Caroline Essert (HDR), Nicolas Magaud, Pascal Mathis (HDR), Julien Narboux
Un médecin : Jimmy Voirin
5 Doctorants : David Braun (Allocataire UNISTRA du 10/2015 au 09/2018), Pierre Boutry (Allocataire UNISTRA du 10/2013 au 09/2016), Noura Hamze (Contrat projets ANR ACouStiC et IHU Haystack du 10/2012 au 09/2015), Rémi Imbach (Allocataire UNISTRA du 10/2010 au 09/2013 (Thèse soutenue le 08/10/2013)), Amir Jaberzadeh (Allocataire CNRS / Région Alsace du 10/2011 au 09/2014 (Thèse soutenue le 13 Février 2015)).

Résultats

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

Nous intéressant au raisonnement géométrique, nous plaçons naturellement à la base de nos travaux l'étude des fondements de la géométrie, leur formalisation pour arriver, autant que faire se peut, à l'automatisation de preuves en géométrie. Ce sujet à la frontière entre les mathématiques pures et l'informatique, n'est étudié que par très peu d'équipes. Un des résultats marquants est la formalisation complète en Coq de la géométrie de Tarski, de l'axiomatique [4-BN12] jusqu'aux coordonnées dans un corps clos [4-BBN16] en passant par une étude approfondie de l'axiomatisation de la notion de parallélisme [5-GBN16,2-BBN15,7-BNSB14] et le théorème de Pappus [2-BN16]. La bibliothèque GeoCoq qui en résulte est librement utilisable par toutes les équipes qui se préoccupent de faire de la preuve formelle dans des domaines incluant la géométrie, comme la géométrie algorithmique. D'une manière annexe, nous avons travaillé sur la génération automatique de propriétés autour du triangle [2-NB16].

En collaboration avec l'équipe de Predrag Janicic de Belgrade, nous avons étudié l'obtention de preuves lisibles à l'aide de la logique cohérente [2-SNJ15, 4-SNBJ14] et nous avons formalisé une méthode de démonstration automatique: la méthode des aires [2-JNQ12].

En collaboration avec Laurent Fuchs, MC Poitiers et Agathe Chollet, nous avons travaillé à la formalisation dans Coq d'un modèle discret du continu basé sur l'analyse non-standard : la droite d'Harthong-Reeb [2-MCF15]. Nous avons établi, d'une part, que la version axiomatisée de cette droite vérifie bien les axiomes de Bridges et, d'autre part, qu'une implantation basée sur les entiers de Laugwitz-Schmieden permet de faire des calculs effectifs. Nous avons appliqué ces résultats à des problèmes simples de géométrie discrète. Nous avons ensuite cherché à utiliser la droite d’Harthong-Reeb pour décrire des transformations linéaires réelles en passant par des suites de transformations linéaires rationnelles [5-ADFL14].

D'autres résultats mettant en oeuvre notre manière d'appréhender les choses pourront être trouvés dans la bibliographie.

Spécification, preuves d'algorithmes et implantation

Ce sujet vient en aval du thème précédent et lui est évidemment étroitement lié. Nous avons travaillé sur la modélisation en Coq de structures de données et d'algorithmes pour la topologie et la géométrie [2-DD14]. La robustesse des algorithmes en géométrie algorithmique est une qualité essentielle dans ce domaine. Pourtant les questions de spécification et certification formelles y sont peu étudiées. Nous avons obtenu des résultats sur des algorithmes de calcul d'enveloppe convexe dans le plan [2-BDM12] et sur la construction incrémentale de diagrammes de Voronoï où les cellules sont décrites en utilisant les modèles topologiques combinatoires développés dans CGoGN. Dans ce dernier cas, nous sommes allés jusqu'à prouver en Coq la correction d'une implantation dans un langage impératif avec pointeurs [4-Dufo14, 4-Dufo14a, 2-Dufo15].

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

Cet aspect de notre thème de recherche est évidemment lié à la question des fondements de la géométrie, mais on y retrouve également beaucoup d'aspects en relation avec l'automatisation des preuves : en effet, résoudre un problème de construction géométrique revient à prouver constructivement un théorème de la forme "quelque soit...il existe ...". L'originalité de notre approche réside dans l'utilisation à plusieurs niveaux de la géométrie pour "guider" des méthodes analytiques (formelles ou non).

Dans les dernières années, nous avons obtenu des résultats dans trois domaines des contraintes géométriques. Ainsi concernant l'aspect spécification des systèmes de contraintes géométriques, nous avons proposé des algorithmes efficaces pour traduire des systèmes de contraintes en systèmes en passant par la géométrie des distances [4-MS13, 2-MS14a]. Avec les travaux de thèse de Rémi Imbach, nous avons proposé des algorithmes nouveaux pour résoudre numériquement des systèmes de contraintes géométriques qui améliorent la vitesse et la robustesse des calculs en guidant des méthodes de suivi de chemin par la géométrie [4-MSI12,2-ISM14, 8-Imba13]. Enfin, nous avons résolu des questions ouvertes dans les corpus de Wernick et de Connelly qui sont relatives aux constructions à la règle et au compas, et ce, en mariant raisonnement géométrique et algèbre [4-MJS15, 2-SM16, 2-SMJ16].

Exemple, problème W108 (Wernick) : construire à la règle et au compas un triangle ABC dont on connaît l’orthocentre, H, le pied Ta de la bissectrice intérieure issue de A et le milieu de [BC], Ma :

Traduction géométrique d’une solution trouvée algébriquement
Construction directe

Formalisation et planification d'opérations chirurgicales

Ce sujet s'appuie sur les travaux précédents notamment en ce qui concerne la démarche, mais il est également lié aux grandes thématiques abordées dans l'équipe IGG. Il se situe en particulier à l’interface de la formalisation et résolution de contraintes géométriques, la modélisation géométrique, l’optimisation, et le traitement d’images médicales. Ces travaux trouvent leurs applications dans l’assistance automatisée à la planification préopératoire et la simulation chirurgicale, et plus particulièrement dans le calcul automatique de trajectoires optimales et sûres en chirurgie percutanée et neurochirurgie stéréotaxique. L'approche suivie est originale et permet de produire du logiciel avec du paramétrage de haut niveau autorisant une grande adaptabilité comme les résultats suivants en attestent.

Nos travaux ont notamment porté sur la prise en compte de la déformabilité des tissus, organes, et outils chirurgicaux dans le calcul de trajectoire, grâce à l’inclusion de simulations biomécaniques dans la boucle d’optimisation [2-HPCE16, 4-HBDC15, 4-BEDC12]. Nous avons également étudié l’optimisation multi-trajectoires simultanées avec prise en compte des interactions entre les multiples outils et leurs effets, et calcul de l’effet résultant par propagation thermique [2-JE15, 4-JE14]. Dans un autre domaine, nous avons travaillé sur la définition précise de contraintes de résolution en stimulation cérébrale profonde [2-EHLA12], avec prise en compte de données de type atlas anatomique-clinique [4-DZHJ14], et définition d’un pipeline de prétraitement automatisé d’images cérébrales [2-DHEF15, 4-DHEF14]. Enfin, nous avons étudié de manière approfondie la question des paramètres d’optimisation : poids des contraintes [2-EFCH15, 4-EMFB12], et influence du choix de la méthode d’optimisation (mono/multicritères) sur la répartition et la pertinence des résultats [4-HVCJ16].

Inclusion de simulations biomécaniques dans la boucle d’optimisation [2-HPCE16]
Résolution de contraintes de positionnement en stimulation cérébrale profonde [2-EHLA12]
Calcul de la propagation thermique en cryoablation [2-JE15]
Points d'insertion possibles sur un front de Pareto [4-HVCJ16]

Perspectives

La période quinquennale qui s'achève a vu la mise en place d'outils et de plateformes qui nous permettront d'aller plus loin dans la conception d'algorithmes robustes et certifiés en géométrie et leur application notamment dans le domaine médical. Par exemple, la formalisation du livre de Tarski en Coq laisse entrevoir un champ d'utilisation immense dans plusieurs domaines dont la géométrie algorithmique ou l'enseignement assisté par ordinateur. L'étude et l'implantation en Coq des concepts autour de la droite d'Hartong-Reeb suit la même approche et pourrait permettre conjointement avec le point précédent une approche globale de la géométrie. Nous avons également développé de nombreux outils permettant de résoudre de manière robuste des systèmes de contraintes en utilisant de manière intensive la géométrie : ces outils pourraient être certifiés puis utilisés pour réaliser des preuves de théorèmes compliqués. Enfin, notre approche par spécification a permis de développer une plateforme stable et complète qui va nous permettre de faire des investigations dans de nouveaux champs de la chirurgie percutanée.