💻 computer science

Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations

Cet article présente un calcul mécanisé sous Lean 4 et un système à double plan (« hurdy-gurdy ») qui permet à des LLM non fiables de générer des traductions auto-certifiées et à fidélité graduée entre des langages de programmation, garantissant qu'un graphe de confiance en évolution continue, vérifié par l'humain, converge vers des questions de programmes décidables avec une assurance toujours croissante.

Auteurs originaux : Christoph Kirsch

Publié 2026-07-20

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Christoph Kirsch

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le dilemme du détective : quand on ne peut pas faire confiance au messager

Imaginez que vous essayiez de résoudre un mystère concernant une machine complexe, comme un moteur de voiture ou le comportement d'un personnage de jeu vidéo. Vous avez une question : « Est-ce que cette voiture va s'écraser si j'appuie sur l'accélérateur à 50 mph ? » Pour y répondre, vous ne pouvez pas simplement regarder la voiture ; vous devez traduire sa mécanique réelle et désordonnée dans un langage qu'un solveur informatique ultra-intelligent peut comprendre, comme une équation mathématique. Mais voici le piège : la personne qui traduit la voiture en mathématiques peut commettre une erreur. Peut-être a-t-elle oublié un engrenage, ou a-t-elle mal compris le fonctionnement des freins. Si le traducteur se trompe, le solveur mathématique vous donnera une réponse parfaite à la mauvaise question.

Dans le monde de l'informatique, c'est le problème de la « traduction ». Nous devons souvent déplacer un programme d'un langage (comme le C ou le Python) vers un autre (comme un casse-tête logique pour un solveur) afin de vérifier s'il est sûr. Traditionnellement, les scientifiques ont tenté de résoudre cela en prouvant que le traducteur était parfait une fois pour toutes, comme on certifie qu'un pont est sûr avant que quiconque ne roule dessus. Mais c'est incroyablement difficile, surtout lorsque les traducteurs sont complexes ou même écrits par une intelligence artificielle. Ce document pose une question différente : et si, au lieu d'essayer de prouver que le traducteur est parfait, nous construisions un système capable de détecter les erreurs du traducteur pendant qu'il travaille ? C'est la différence entre faire confiance à un guide unique pour vous guider à travers une forêt et avoir une équipe de guides qui vérifient les cartes les uns des autres, avec une règle stipulant que s'ils ne sont pas d'accord, vous vous arrêtez et cherchez qui a tort.

La machine « Hurdy-Gurdy » : une usine pour des réponses dignes de confiance

Ce document présente un système appelé hurdy-gurdy (nommé d'après un instrument de musique qui produit des mélodies, mais ici, il produit des réponses). Les auteurs, dirigés par Christoph Kirsch, proposent une nouvelle façon de gérer les programmes informatiques : les traiter comme une partie de « téléphone arabe » où chaque étape est vérifiée, et où chaque réponse est accompagnée d'un reçu.

L'idée centrale est simple mais puissante : ne faites pas confiance au traducteur ; faites confiance au processus.

Imaginez que vous ayez une question sur un programme écrit en C. Au lieu de l'envoyer à un seul traducteur, le système l'envoie sur deux chemins différents.

La Traduction : Le programme est traduit en un langage logique plus simple (comme transformer un roman en une équation mathématique).
La Double Vérification : Le système exécute le programme original et la version traduite côte à côte. Il vérifie s'ils se comportent de la même manière. Si c'est le cas, parfait ! Si ce n'est pas le cas, le système indique précisément l'étape où ils ont divergé, comme un arbitre sifflant une faute au moment exact où un joueur commet une faute.
L'astuce du « Témoin » : Si le solveur dit : « Oui, un crash est possible », le système ne se contente pas de croire le solveur. Il prend la « preuve » (les conditions spécifiques qui causent le crash) et la fait circuler à rebours à travers la traduction. Il injecte ces conditions dans le programme original. Si le programme original plante réellement, alors la réponse est 100 % réelle. Le système a « rejoué » la scène du crime.

Les deux plans : Construction et Utilisation

Le système possède deux modes distincts, comme un atelier de fabrication et une salle d'exposition :

Le Plan d'Utilisation (La Salle d'Exposition) : C'est là que les réponses se produisent. Ici, une IA (ou un humain) pose des questions. Le système ne devine pas ; il choisit un itinéraire, vérifie la traduction, et si la réponse est « Oui, c'est possible », il lance la relecture pour le prouver. Si la réponse est « Non, c'est impossible », le système s'appuie sur une pile de vérifications : plusieurs traducteurs, plusieurs solveurs, et même des certificats mathématiquement vérifiés pour en être sûr.
Le Plan d'Évolution (L'Usine) : C'est là que le système grandit. Si le système ne peut pas répondre à une question, il ne se contente pas d'abandonner. Il note pourquoi il a échoué (par exemple : « Nous n'avons pas de traducteur pour ce type spécifique de boucle »). Il utilise ensuite une IA pour construire un nouveau traducteur afin de combler cette lacune. Une fois construit, le nouveau traducteur est testé par rapport aux anciens. S'il réussit, il est ajouté au registre. S'il échoue, il est corrigé. Cette boucle tourne indéfiniment, rendant le système plus intelligent et plus digne de confiance au fil du temps, mais crucialement, le processus de croissance ne répond jamais aux questions lui-même. Il ne fait que construire les outils pour y répondre.

Le rebondissement des « Auteurs non fiables »

La partie la plus surprenante du document est que les traducteurs eux-mêmes ont été construits par des agents d'IA non fiables. Les auteurs n'ont pas codé les traducteurs à la main ; ils ont demandé à des modèles d'IA de les écrire sur la base d'une description d'une page. Habituellement, cela serait un désastre. Mais parce que le système vérifie chaque étape, les erreurs de l'IA sont immédiatement détectées.

Par exemple, lors d'un test, un traducteur d'IA a omis une instruction spécifique, provoquant un comportement différent du programme original. La « vérification carrée » du système (la comparaison côte à côte) a repéré l'erreur instantanément, localisant la ligne exacte et la variable exacte qui posaient problème. Le système a ensuite corrigé le traducteur. Le document montre que même avec des auteurs d'IA qui peuvent se tromper, l'architecture du système garantit que les réponses finales sont dignes de confiance.

Ce que le système a trouvé (et n'a pas trouvé)

Les auteurs ont testé ce système sur un instantané de leur travail de juillet 2026. Voici ce qu'ils ont mesuré :

Couverture : Ils ont réussi à traduire des programmes de 13 langages différents (incluant le C, le Python et même des réseaux de réactions chimiques) en solveurs logiques. Pour le langage de processeur RISC-V, ils ont couvert 96 sur 96 types d'instructions spécifiques, ce qui signifie que le système pouvait gérer chaque instruction de cet ensemble sans perdre le fil.
Accord : Lorsqu'ils ont envoyé la même question via deux chemins de traduction différents (l'un basé sur un manuel, l'autre sur un modèle formel), les réponses concordaient 100 % du temps sur les cas de test.
Défauts détectés : Le système a détecté 24 défauts spécifiques dans ses propres traducteurs et outils. Certains étaient de simples fautes de frappe, d'autres des erreurs de logique où l'IA avait mal compris le fonctionnement d'une instruction informatique. Crucialement, le système a trouvé ces erreurs sans qu'un humain n'ait à examiner le code.
Le « Point aveugle » : Le système a également identifié une limite. Si deux traducteurs différents commettent la même erreur (parce qu'ils ont tous deux mal compris la même règle), le système ne peut pas la détecter. C'est ce qu'on appelle une « défaillance de mode commun ». Le document admet que c'est un risque, mais le système est conçu pour le minimiser en utilisant des sources de traduction diversifiées.
Joueurs LLM : Ils ont testé si une IA pouvait utiliser le système pour répondre à des questions. Dans une expérience, une IA sans outils a répondu correctement à 7 questions sur 8, mais a deviné pour la plus difficile. L'IA avec le système a obtenu 8 sur 8, et chaque réponse était accompagnée d'une preuve vérifiée par machine.

L'essentiel

Ce document ne prétend pas avoir résolu tous les problèmes de sécurité informatique. Il ne dit pas que les traducteurs d'IA sont désormais parfaits. Au contraire, il prouve que vous pouvez construire un système digne de confiance à partir de composants non fiables.

En traitant chaque traduction comme une erreur potentielle et en construisant un « cliquet » qui ne permet que l'amélioration durable, le système crée une échelle de confiance. Si la question est « Cela peut-il arriver ? », le système peut rejouer l'événement pour le prouver. Si la réponse est « Non, cela ne peut pas arriver », le système s'appuie sur une chaîne de vérifications indépendantes et de certificats mathématiquement vérifiés pour en être certain.

Les auteurs concluent que cette approche — utiliser un graphe de routes, vérifier chaque étape et rejouer les preuves — est un moyen viable de gérer la complexité des logiciels modernes, même lorsque les personnes (ou les IA) qui construisent les outils sont faillibles. C'est un passage de « la confiance envers l'auteur » à « la confiance envers l'architecture ».

Résumé technique : Auteurs non fiables, Réponses de confiance

Énoncé du problème

Le document traite du défi fondamental consistant à répondre à des questions sur des programmes (par exemple, la de l'accessibilité, la validité d'assertions) lorsque les outils utilisés pour traduire et analyser ces programmes sont considérés comme non fiables. Les approches traditionnelles reposent soit sur la preuve de la correction d'un traducteur unique (par exemple, CompCert), soit sur la validation de chaque exécution d'un traducteur unique. Cependant, ces méthodes supposent un "bord" de traduction unique. L'article soutient que dans un écosystème complexe impliquant de multiples langages sources, des cibles de raisonnement diverses et des auteurs potentiellement non fiables (y compris des LLM), le processus de traduction forme un graphe de nombreux langages et routes. Dans ce graphe, chaque traduction est un point de défaillance potentiel. Le problème central est de savoir comment composer ces traductions hétérogènes, construites de manière indépendante et potentiellement non fiables, en un système capable de fournir des réponses de confiance sans exiger la preuve universelle de chaque composant.

Méthodologie : Le calcul des traductions à fidélité graduée

Les auteurs proposent un calcul formel et une implémentation de plateforme appelée hurdy-gurdy. La méthodologie repose sur deux "plans" distincts se rejoignant dans un registre partagé :

1. Le Plan d'Utilisation (Répondre aux questions)

Ce plan traite la traduction comme un graphe où les nœuds sont des langages et les arêtes sont des paires de traduction.

La Paire et le Carré : L'unité fondamentale est une paire $(A, B)$ $(A, B)$ composée d'un traducteur $T$ $T$ , d'un retour cible-source $\Lambda$ $Λ$ , et d'interprètes partagés. Une paire est validée via un carré commutatif directionnel :
- Exactitude : Le comportement de la source est égal au comportement de la cible ramené (une bisimulation sur les observables conservés).
- Sur-approximation : Le comportement de la source est simulé par le comportement de la cible (autorisant des comportements spécieux mais préservant les comportements de la source).
- Décidabilité : Pour tout programme spécifique, le carré est vérifié en exécutant les deux côtés et en comparant les traces projetées. En cas de divergence, l'échec est localisé à une étape et un observable spécifique.
Composition et Contrats : Les routes sont des chemins composés à travers le graphe. Le contrat d'une route est la rencontre composante par composante (componentwise meet) des contrats de ses sauts, définie par quatre axes :
- Classe d'assurance : Une hiérarchie allant de aucun à rejouer, par exécution, et universel.
- Direction : Exactitude ou sur-approximation.
- Observables conservés : L'intersection des observables préservés par chaque saut (la perte s'accumule).
- Coût : Mesuré en temps d'exécution.
Mécanismes de Confiance :
- Rétablissement par exécution : Même un saut "de confiance" peut être validé dynamiquement si l'oracle du carré réussit pour l'exécution spécifique.
- Corroboration par branche : Si deux routes dérivées indépendamment (préfixes divers) concordent sur un verdict, la preuve est plus forte que le grade individuel de chaque route.
- Asymétrie Existentielle/Universelle :
  - Réponses Existentielles (Atteignable) : Auto-certifiantes. Le témoin du solveur est transporté en retour et rejoué dans l'interprète de la source. Si le replay présente le comportement, la réponse est vraie indépendamment des erreurs du traducteur (Base de confiance : Adéquation de l'interprète de la source).
  - Réponses Universelles (Inatteignable) : Non auto-certifiantes. Elles reposent sur la composition des grades, l'accord des branches et des certificats formels (par exemple, des preuves DRAT vérifiées par des vérificateurs certifiés).

2. Le Plan d'Évolution (Croissance du Graphe)

Ce plan gère la croissance du graphe de traduction.

Génération non fiable : Les paires sont implémentées par des agents LLM indépendants à partir de briefs.
Le Cliquet (Ratchet) : Le système impose un modèle de croissance additive. Les nouvelles contributions doivent étendre la couverture sans invalider les verdicts antérieurs.
Demande et Enregistrement : Les questions sans réponse sont enregistrées comme "demande". Des recommandations pour de nouvelles paires sont générées sur la base de preuves. L'enregistrement humain est l'ultime barrière ; le système ne répond pas de manière autonome aux questions, il accroît seulement sa capacité à le faire.

Contributions Clés

Un calcul de paires directionnelles à fidélité graduée : Un cadre formel où l'exactitude est un cas particulier de la sur-approximation, et où la composition est définie par une rencontre de type "maillon le plus faible" à travers l'assurance, la direction, la perte et le coût.
L'Algèbre des Contrats : Un mécanisme pour composer des preuves hétérogènes. L'article formalise comment les vérifications "par exécution" et les garanties "universelles" se combinent, et comment la perte (observables rejetés) s'accumule le long d'une route.
L'Asymétrie Existentielle/Universelle : Un principe architectural distinguant les réponses qui transportent des témoins (auto-certifiantes via le replay de la source) de celles qui n'en transportent pas (nécessitant un grade de confiance et des certificats).
L'Architecture à Deux Plans : Une séparation entre les plans d'utilisation (répondre) et d'évolution (construire), permettant à des agents non fiables de construire le système tandis que l'architecture garantit la confiance par des vérifications croisées, de la diversité et un mécanisme de cliquet.
Mécanisation : Le cœur compositionnel, incluant le théorème de collage, la localisation et les théorèmes d'asymétrie de bout en bout, est mécanisé dans Lean 4 (environ 1 250 lignes) avec un audit d'axiomes rigoureux.

Résultats et Évaluation

L'article évalue un "instantané de juillet 2026" de la plateforme hurdy-gurdy, entièrement construite par des agents LLM sans revue sémantique humaine du code.

Couverture et Correction : Le système couvre 13 langages et 15 paires enregistrées. Il a réussi à composer des routes pour RISC-V, AArch64, eBPF, Wasm, EVM, Python, et d'autres.
- Accord de Branche : Deux routes pour RISC-V (dérivée manuellement vs dérivée de Sail) et AArch64 ont concordé sur les 12 questions de de l'accessibilité testées, y compris les verdicts universels (inatteignable).
- Benchmark de Conformité : Un benchmark dérivé de 78 questions de la suite de tests RISC-V a été résolu avec un accord de 100 % entre les routes et une correction de 100 % par rapport à la vérité terrain.
Détection de Défauts : L'architecture a détecté 24 défauts dans le code généré par les LLM, notamment :
- Un mauvais décodage silencieux d'instructions (ex: MUL interprété comme ADD) où l'interprète et le traducteur étaient tous deux en erreur (un "angle mort" capté uniquement par la diversité externe).
- Des représentations intermédiaires malformées tolérées par un solveur mais rejetées par d'autres.
- Des failles dans l'instrumentation de la plateforme elle-même (ex: un adaptateur de vérificateur acceptant des preuves erronées).
Expériences de Taux d'Échappement : Des mutations sémantiques injectées dans le traducteur RISC-V ont été testées contre les barrières du système.
- La "suite de carrés" (sondes conjointes) a capté 51/55 mutants.
- Les 4 restants ont été captés par le benchmark dérivé.
- Zéro échappement n'a été observé lors du dernier tour, bien que les auteurs notent que cela mesure la famille de mutations, et non un taux d'échappement nul pour toutes les erreurs possibles.
- Les défaillances de mode commun (où les deux jambes d'un carré sont erronées de manière identique) ont été captées uniquement par la branche diverse (route Sail) ou par des différentiels externes, validant la nécessité d'ancres sémantiques indépendantes.
Expérience du Joueur LLM : Un agent LLM a été chargé de répondre à des questions en utilisant la plateforme.
- Dans une seconde itération (v2), le joueur LLM a obtenu 8/8 réponses correctes sur des questions difficiles de de l'accessibilité BTOR2, tandis qu'un LLM non assisté a obtenu 7/8.
- Crucialement, les réponses du joueur LLM étaient accompagnées d'artefacts de preuve vérifiés par machine (ex: témoins rejoués, certificats LRAT), alors que le LLM non assisté reposait sur son "affirmation" et des scores de confiance.
Performance : Le surcoût de la discipline (vérification de chaque saut, replay des témoins) est faible par rapport à l'appel du solveur. La traduction prend des millisecondes ; le solveur domine le temps de calcul.

Signification et Revendications

L'article affirme que la confiance dans la traduction peut être fabriquée par l'architecture plutôt qu'en faisant confiance à l'auteur.

Position de Système Distribué : Il traite les traducteurs comme des composants sujets à la défaillance, contenant l'erreur par des projections déclarées, des vérifications décidables et des routes indépendantes, plutôt que de tenter de la prévenir via une preuve universelle.
Le "Cliquet" de la Confiance : Le système est conçu pour évoluer. La couverture et l'assurance croissent de manière monotone ; les verdicts antérieurs sont préservés même lors de l'expansion du graphe.
Portée Modeste : Les auteurs précisent explicitement que le système est un "instantané de capacité daté". Il ne prétend pas résoudre l'indécidabilité ou remplacer toute la vérification formelle. Le niveau "prouvé" n'est habité que pour des questions spécifiques et bornées avec des certificats formels. Le système repose sur l'exécution empirique de l'adéquation de l'interprète et des hypothèses de diversité structurelle.
L'Asymétrie : L'article conclut que pour les réponses existentielles, la confiance est "presque gratuite" (via le replay), tandis que pour les réponses universelles, le système doit consciemment "acheter" l'assurance via des niveaux gradués, des branches et des certificats.

Le travail pose qu'un système construit sur ces principes peut permettre à des auteurs non fiables (humains ou IA) de contribuer à une infrastructure de raisonnement vérifiée, à condition que l'architecture impose des vérifications croisées rigoureuses et des contrats compositionnels.