Poste de pilotage pour la démonstration automatique

Notre programme de recherche fait tourner de longs travaux automatisés. Des modèles de langue proposent des énoncés mathématiques, d'autres modèles tentent de les démontrer, et un vérificateur formel de preuves, le noyau Lean, accepte ou rejette chaque preuve. Une exécution dure des jours. Avant ces écrans, le seul moyen de savoir ce qu'une exécution avait fait était de lire ses journaux.

Le poste de pilotage est une vue en direct de ces exécutions. Il diffuse l’état de l’exécution à mesure qu’il change : combien de résultats le vérificateur a certifiés, combien d’énoncés restent ouverts, ce que chaque modèle produit pour ce qu’il coûte, et un graphe généalogique qui rattache chaque résultat certifié à la branche de modèle qui l’a produit. Un clic sur un nœud ouvre sa fiche. Aucun chiffre à l’écran n’est saisi à la main : chacun est lu dans le registre que tient le vérificateur.

L’écran répond d’abord aux questions qu’on se pose : qu’est-ce qui a été certifié, qu’est-ce qui reste ouvert, quel modèle vaut ce qu’il coûte. Le détail de chaque résultat reste à un clic au lieu d’encombrer le premier écran.

Le logiciel lui-même

Capture de l’outil en fonction. Les noms des théorèmes et des modèles sont floutés. L’interface est montrée en anglais.

À quoi ça tient

Les écrans ne montrent que ce qu'un vérificateur indépendant a déjà accepté. Le poste de pilotage ne décide pas si une preuve est correcte : c'est le noyau qui en décide, et le poste compte ses verdicts. C'est cette séparation qui permet à quelqu'un qui ne sait pas lire les preuves de se fier quand même à un chiffre affiché.

Le poste est écrit en Python et en JavaScript simples, sans cadriciel ni bibliothèque tierce : il démarre en une seconde environ sur toute machine qui a Python. La même approche vaut pour un tableau de bord sur un processus d’affaires : lire la source de vérité, ne jamais la ressaisir.