Towards a Certifying Grounder

Imaginez que vous soyez un détective essayant de résoudre un mystère massif et complexe. Vous avez un ensemble d'indices écrits dans un code complexe de haut niveau que seuls quelques experts peuvent lire. Pour percer l'affaire, vous devez traduire ces indices en une liste de contrôle simple, étape par étape, qu'un ordinateur peut suivre. Ce processus de traduction est appelé « ancrage » (grounding). C'est comme transformer un roman rempli de métaphores en une liste stricte d'instructions : « Si le suspect est dans la cuisine, vérifiez la fenêtre ; s'il est dans le jardin, vérifiez la clôture. »

Pendant des décennies, les ordinateurs qui résolvent ces énigmes sont devenus incroyablement rapides et intelligents. Cependant, il existe un problème caché : parfois, l'étape de traduction (l'ancrage) commet une erreur, ou l'ordinateur s'embrouille et invente un indice qui n'était pas là. Si la traduction est fausse, la réponse finale est fausse, peu importe la perfection de la logique de l'ordinateur. Dans le monde réel, cela compte énormement. Si un ordinateur aide à planifier une mission de navette spatiale ou à faire correspondre des donneurs de reins avec des patients, une infime erreur dans la traduction pourrait mener à un désastre. Nous avons besoin d'un moyen de savoir avec certitude que l'ordinateur n'a pas simplement « deviné » la bonne réponse, mais qu'il a réellement suivi les règles parfaitement du début à la fin. C'est là qu'intervient l'idée du « journal de preuve » (proof logging) — comme un détective écrivant chaque étape de son raisonnement afin qu'un second détective, plus simple, puisse vérifier le travail et dire : « Oui, tu l'as bien fait. »

Ce document présente un nouveau système appelé CertiFOX qui apporte ce « journal de preuve » à l'étape de la traduction elle-même. Les auteurs, une équipe de la KU Leuven et de la Vrije Universiteit Brussel, ont construit un cadre qui ne se contente pas de résoudre des problèmes ; il écrit un certificat prouvant que la traduction du mystère de haut niveau vers la liste de contrôle de bas niveau a été effectuée correctement. Ils ont créé trois outils principaux : un nouveau langage pour écrire ces certificats, un « ancreur » (le traducteur) qui écrit le certificat pendant qu'il travaille, et un « vérificateur » (le second détective) qui lit le certificat pour vérifier le travail. Leurs expériences montrent que ce système fonctionne aussi bien que les outils de pointe actuels, et que le temps supplémentaire nécessaire pour écrire et vérifier la preuve est très faible — juste un petit facteur constant. Ils n'ont pas seulement suggéré que cela pourrait fonctionner ; ils l'ont construit, testé sur de vraies énigmes, et prouvé qu'il peut accomplir la tâche sans ralentir excessivement les choses.

Le dilemme du détective : Faire confiance au traducteur

Plongeons plus profondément dans l'histoire. Dans le monde de l'informatique, plus précisément dans un domaine appelé « résolution déclarative », les gens décrivent des problèmes en utilisant un langage de haut niveau qui ressemble à des mathématiques ou à de la logique. C'est lisible et élégant. Mais les ordinateurs ne parlent pas directement le « langage de la logique élégante » ; ils parlent un langage de bas niveau très rigide (comme une longue liste d'énoncés vrai/faux). Pour passer de l'idée élégante à la liste rigide, un programme spécial appelé ancreur (grounder) fait le gros du travail. Il prend les règles de haut niveau et les développe en chaque cas spécifique possible.

Voyez cela comme une recette. La théorie de haut niveau est la recette : « Cuire un gâteau pour chaque invité. » L'ancreur est le chef qui regarde la liste des invités et écrit les instructions spécifiques : « Cuire un gâteau pour Alice. Cuire un gâteau pour Bob. Cuire un gâteau pour Charlie... » Si le chef compte mal les invités ou oublie un nom, la fête est gâchée. Le problème est que ces chefs (les ancreurs) sont incroyablement complexes. Ils utilisent des astuces et des raccourcis ingénieux pour gérer de grandes listes d'invités rapidement. Parce qu'ils sont si complexes, il est difficile d'être sûr à 100 % qu'ils ne commettent pas d'erreur. Si le chef fait une erreur, l'ordinateur pourrait dire : « Nous avons trouvé une solution ! » alors qu'en réalité, aucune solution n'existe, ou inversement.

La solution CertiFOX : La trace écrite

Les auteurs de ce document ont réalisé que, bien que nous soyons devenus bons pour vérifier la réponse finale (l'ordinateur a-t-il trouvé la solution ?), nous n'avons pas été bons pour vérifier la traduction (le chef a-t-il écrit la liste correctement ?). Ils voulaient combler ce « fossé de confiance ».

Pour ce faire, ils ont construit CertiFOX. Imaginez CertiFOX comme une nouvelle sorte de cuisine où le chef ne se contente pas de cuisiner ; il tient également un journal détaillé, étape par étape, de chaque mouvement qu'il fait.

1. GroundFOX : C'est le nouveau chef. Il prend la recette de haut niveau et la traduit en une liste de bas niveau. Mais pendant qu'il travaille, il écrit une « preuve » dans un format spécial. Il ne dit pas seulement « J'ai fait un gâteau pour Alice » ; il dit : « J'ai regardé la liste des invités, j'ai vu Alice, et j'ai appliqué la Règle 4 pour écrire 'Cuire pour Alice'. »
2. Le format de preuve : C'est le langage du journal. Les auteurs ont conçu un ensemble spécifique de règles (comme une grammaire) que le chef doit suivre. Ces règles sont assez simples pour qu'un ordinateur puisse facilement les lire et vérifier que chaque étape suit logiquement la précédente.
3. CheckFOX : C'est l'inspecteur indépendant. Il ne cherche pas à résoudre l'énigme lui-même. Il se contente de lire le journal du chef et de vérifier les calculs. « Le chef a-t-il vraiment vu Alice dans la liste ? Oui. La règle disait-elle de cuisiner pour elle ? Oui. D'accord, cette étape est correcte. »

Comment ça marche : La magie des « Gardes »

L'une des astuces ingénieuses utilisées par les auteurs est ce qu'ils appellent la Forme Normale d'Ancrage (GNF). En langage clair, c'est une façon d'organiser les règles pour que le chef puisse être plus intelligent. Habituellement, un chef pourrait devoir vérifier chaque personne dans le monde pour voir si elle est une invitée. C'est lent. Mais avec la GNF, les règles incluent des « gardes ».

Imaginez un garde à la porte qui ne laisse entrer que les personnes possédant un badge spécifique. Le chef n'a besoin de vérifier que les personnes qui passent le garde. Dans le langage du document, cela signifie que l'ancreur peut ignorer les détails non pertinents. Par exemple, si la règle est « Si une personne est un pigeon, trouver un trou », l'ancreur ne regarde que les pigeons, pas les chats ou les rochers. Cela rend la traduction beaucoup plus rapide et la preuve beaucoup plus courte. Les auteurs ont montré qu'en utilisant ces gardes, ils pouvaient garder le « journal » (la preuve) compact et gérable, même pour de gros problèmes.

Le test grandeur nature : Est-ce que cela fonctionne vraiment ?

L'équipe ne s'est pas contentée de construire cela en théorie ; elle l'a mis à l'épreuve. Ils ont pris un ensemble de puzzles standards (comme la coloration de cartes, l'appariement de mariages stables et la recherche de motifs dans les nombres) et les ont passés dans leur nouveau système. Ils ont comparé leur nouveau chef (GroundFOX) à deux autres chefs célèbres : IDP-Z3 et pyclingo.

Les résultats sont impressionnants.

• Vitesse : Le nouveau chef est presque aussi rapide que les experts. Dans certains cas, il était un peu plus lent, mais dans d'autres, il était très compétitif. Il a réussi à résoudre presque tous les puzzles dans les limites de temps imparties.
• Le coût de la preuve : La question la plus importante était : « À quel point est-on plus lent parce qu'on écrit un journal ? » La réponse était : « Pas beaucoup. » Le temps supplémentaire pour écrire la preuve était infime. Et quand l'inspecteur (CheckFOX) a lu le journal, cela n'a pris que 2 à 3 fois plus de temps que la cuisine elle-même. C'est un prix très faible à payer pour une certitude totale.
• Mémoire : Curieusement, le nouveau système était meilleur pour ne pas manquer de mémoire sur certains puzzles très difficiles par rapport aux autres outils.

Les auteurs ont également examiné la taille des « journaux » (les preuves). Ils ont constaté que pour la plupart des puzzles, les journaux étaient raisonnables. Cependant, pour un type spécifique de puzzle (RamseyNumbers), les journaux sont devenus énormes. Pourquoi ? Parce que ce puzzle n'utilisait pas les « gardes » efficacement, forçant le chef à écrire des millions d'étapes. Cela leur a appris que l'utilisation des bons « gardes » est cruciale pour garder la preuve compacte.

L'essentiel

Le document conclut que CertiFOX est un moyen réalisable et prometteur de rendre la résolution déclarative digne de confiance. Il prouve que vous pouvez avoir un système qui non seulement résout des problèmes difficiles, mais fournit également une garantie mathématique que la traduction a été effectuée correctement.

Les auteurs veillent à ne pas prétendre avoir résolu chaque problème. Ils notent que leur système actuel fonctionne mieux sur un type spécifique de logique (appelée GNF) et qu'ils doivent encore l'étendre pour gérer des langages encore plus complexes. Ils mentionnent également que l'« inspecteur » (CheckFOX) peut utiliser beaucoup de mémoire sur des preuves très volumineuses, ce qui est un point qu'ils prévoient de corriger à l'avenir.

Mais le message central est clair : nous pouvons enfin combler le fossé entre les idées de haut niveau que nous écrivons et les réponses de bas niveau que les ordinateurs nous donnent. En ajoutant un contrôle simple et indépendant, nous pouvons arrêter de deviner et commencer à savoir que nos solutions informatiques sont véritablement correctes. C'est comme donner à chaque détective informatique un partenaire de confiance qui vérifie le travail, garantissant que, lorsque nous comptons sur ces machines pour des décisions de vie ou de mort, nous pouvons leur faire entièrement confiance.