Animation, Verification and Visualisation of Prolog Transition Systems with ProB

Imaginez que vous soyez un détective tentant de résoudre un mystère, mais qu'au lieu d'une scène de crime, votre « crime » soit un morceau de code informatique qui pourrait cacher un bug. Dans le monde de l'informatique, on appelle cela la vérification formelle. C'est comme construire une carte mathématique parfaite de la manière dont un programme devrait se comporter, puis vérifier chaque étape pour s'assurer que le programme ne s'égare pas ou ne plante pas. Habituellement, cela implique des mathématiques complexes que seuls les experts peuvent lire. Mais et si vous pouviez transformer ces mathématiques arides en un jeu vidéo vivant et vibrant ? C'est là que réside la magie de Prolog, un langage de programmation qui pense en termes de puzzles logiques plutôt qu'en instructions standards. Lorsque vous combinez Prolog avec un outil appelé PROB, vous obtenez un « vérificateur de modèles » (model checker) — un robot super intelligent capable de surveiller votre puzzle logique se dérouler, de repérer les erreurs, et même de vous laisser parcourir l'histoire étape par étape pour voir exactement où les choses tournent mal.

Ce document traite de l'octroi à ce robot d'une mise à niveau majeure. Les auteurs, une équipe de l'Université Heinrich Heine de Düsseldorf, ont pris un outil existant appelé PROB (qui parle déjà le Prolog) et lui ont ajouté un tout nouvel ensemble de super-pouvoirs. Considérez cela comme le passage d'un carnet de croquis en noir et blanc à un studio de cinéma interactif en haute définition. Ils ont rendu la visualisation de ce qui se passe plus facile, ont ajouté un moyen de simuler des milliers de parties en quelques secondes pour tester des stratégies, et ont même créé un système où vous pouvez mettre l'action en pause, donner une instruction spécifique à l'ordinateur, et le regarder réagir. Ils ont testé ces nouvelles fonctionnalités en transformant le classique jeu de Puissance 4 en un puzzle logique, opposant différents « cerveaux » informatiques pour voir qui gagne. Le résultat est une boîte à outils qui fait en sorte que la vérification de la logique informatique complexe ressemble plus à jouer à un jeu qu'à faire ses devoirs.

La Magie de la Carte Logique « Vivante »

En son cœur, le document décrit comment prendre un ensemble de règles écrites en Prolog (un langage qui ressemble à une liste d'énoncés du type « si ceci, alors cela ») et les transformer en un système de transition. Imaginez un jeu de société où chaque case est un « état » (comme « Le feu de signalisation est rouge ») et chaque mouvement est une « transition » (comme « Passer au vert »). Autrefois, PROB pouvait charger ces règles et vous permettre de cliquer sur un bouton pour passer d'une case à l'autre, montant ainsi le chemin. Mais l'expérience était un peu maladroite.

Les auteurs ont considérablement poli cette expérience. D'abord, ils ont nettement amélioré les visuels. Auparavant, vous voyiez peut-être simplement une liste de texte disant « État : Rouge ». Désormais, ils ont intégré des outils capables de dessiner de véritables images. Si vous modélisez un feu de signalisation, l'outil peut maintenant afficher un véritable cercle rouge brillant sur votre écran. Si vous modélisez une partie d'échecs, il peut afficher l'échiquier avec les pièces à leurs emplacements exacts. Plus cool encore, ils ont ajouté des visualisations interactives : vous pouvez faire un clic droit sur une pièce dans l'image, et l'outil vous montrera tous les mouvements légaux que vous pouvez effectuer, tout comme dans un vrai jeu vidéo. Ils ont également créé une fonctionnalité pour exporter ces histoires visuelles sous forme de fichiers HTML, afin que vous puissiez partager votre « film » du puzzle logique avec n'importe qui, même si cette personne ne possède pas le logiciel spécialisé.

La Fonctionnalité « Pause et Demande »

L'un des nouveaux tours les plus excitants est ce qu'ils appellent les transitions symboliques. Imaginez que vous jouez à un jeu contre un ordinateur, mais que l'ordinateur reste bloqué parce qu'il ne sait pas quel mouvement vous voulez faire ensuite. Par le passé, l'ordinateur pouvait simplement deviner ou s'arrêter. Désormais, l'outil peut faire une pause et dire : « Hé, j'ai besoin qu'un humain décide de cette partie ! ». Il attend que vous saisissiez une valeur spécifique (comme « Déplace le cavalier en F3 ») puis reprend l'histoire. C'est crucial pour tester une logique complexe, comme la preuve d'un théorème mathématique, où un humain peut devoir faire un choix qu'un ordinateur ne peut pas prédire de lui-même.

Ils ont également amélioré la relecture de trace (trace replay). Voyez cela comme une fonction « Sauvegarder la partie ». Si vous trouvez une séquence parfaite de mouvements qui résout un problème, vous pouvez la sauvegarder. Plus tard, vous pouvez charger ce fichier de sauvegarde, et l'outil rejouera exactement les mêmes mouvements étape par étape. C'est crucial pour s'assurer que si vous corrigez un bug aujourd'hui, vous n'en avez pas accidentellement cassé un autre demain. La nouvelle version enregistre ces relectures dans un format intelligent (JSON) qui se souvient exactement de l'état dans lequel vous vous trouviez, de sorte que la relecture soit parfaite à chaque fois.

Le Simulateur de « Million de Parties »

L'ajout le plus puissant est peut-être la capacité de lancer des simulations de Monte Carlo. C'est une façon sophistiquée de dire : « Jouons au jeu un million de fois pour voir ce qui se passe ». Les auteurs ont connecté PROB à un simulateur appelé SIMB. Au lieu de simplement regarder une seule partie, vous pouvez dire à l'ordinateur de jouer au Puissance 4 10 000 fois de suite, laissant différentes stratégies s'affronter.

Ils ont utilisé cela pour tester trois « cerveaux » différents pour le Puissance 4 :

1. Aléatoire (Random) : Un joueur qui choisit un mouvement sans réfléchir.
2. Minimax : Une IA classique qui regarde quelques coups à l'avance pour trouver le meilleur chemin.
3. MCTS (Monte Carlo Tree Search) : Une IA plus intelligente qui simule de nombreux futurs possibles pour prendre sa décision.

Les résultats ont été fascinants. Lorsque le joueur Aléatoire affrontait Minimax, le joueur Aléatoire gagnait environ 55,7 % du temps s'il commençait, mais ce chiffre tombait à 7,3 % quand Minimax commençait. Cependant, lorsque Minimax affrontait MCTS, le joueur MCTS l'écrasait, gagnant environ 99 % des parties. Les auteurs ont noté que leur joueur Minimax était un peu faible car il ne regardait que deux coups à l'avance (une recherche superficielle), ce qui explique pourquoi il perdait si mal face à l'avancé MCTS.

Ils ont également mesuré le temps de ces parties. Les joueurs Aléatoire et Minimax étaient rapides, terminant 10 000 parties en moins de 20 minutes. Mais le joueur MCTS était un peu plus lent, prenant plusieurs heures pour effectuer le même nombre de parties car il faisait beaucoup plus de réflexion. Curieusement, ils ont trouvé que le joueur MCTS n'avait besoin que de 9,7 coups en moyenne pour battre le joueur Aléatoire, tandis que Minimax en avait besoin de 18,0.

Pourquoi cela importe

Il ne s'agit pas seulement de jouer à des jeux. Les auteurs montrent que ces outils sont parfaits pour l'enseignement. Imaginez un étudiant apprenant à écrire du code ; au lieu de simplement fixer un écran de texte, il peut voir son code prendre vie sous forme d'animation visuelle. S'il fait une erreur, il peut voir le « feu de signalisation » devenir rouge ou la « pièce d'échecs » disparaître, ce qui rend beaucoup plus facile la compréhension de ce qui a mal tourné.

Le document souligne également que ce système est excellent pour construire des interprètes. Un interprète est comme un traducteur qui permet à un langage de programmation de parler à un autre. En utilisant les nouvelles fonctionnalités de PROB, les étudiants et les chercheurs peuvent facilement construire des traducteurs pour d'autres langages (comme Java ou WebAssembly) et immédiatement les tester en les regardant s'exécuter dans le visualiseur.

En fin de compte, les auteurs ne prétendent pas avoir résolu tous les problèmes de l'informatique. Ils suggèrent qu'en rendant ces outils logiques plus visuels, interactifs et capables de lancer des simulations massives, nous pouvons détecter les bugs plus tôt, mieux enseigner aux étudiants et comprendre plus profondément les systèmes complexes. Ils évoquent même un futur où ces outils pourraient être utilisés pour entraîner des agents d'IA via l'apprentissage par renforcement, laissant l'ordinateur apprendre à jouer à des jeux (ou à résoudre des puzzles logiques) par essais et erreurs, tout comme un humain le ferait. Mais pour l'instant, la victoire principale est de transformer le monde aride et abstrait des preuves logiques en un terrain de jeu où l'on peut voir, toucher et jouer avec les règles.