Résumé technique : Le fossé de fidélité dans l'autoformalisation par les LLM

1. Définition du problème : Le fossé de fidélité (Faithfulness Gap)

Les systèmes modernes d'autoformalisation, qui traduisent les mathématiques en langage naturel (LN) vers des assistants de preuve formels (par exemple, Lean 4, Isabelle/HOL), sont actuellement limités non pas par la fluidité de la traduction, mais par la fidélité. Bien qu'une énoncé formel généré puisse être syntaxiquement correct (vérification de type) et même prouvable, il peut encoder un théorème sémantiquement distinct de l'énoncé initial en LN.

Les auteurs identifient cela comme le fossé de fidélité. Contra irement au code, où les tests unitaires fournissent un oracle exécutable, la formalisation mathématique manque d'un pont direct entre le LN (interprété sous des conventions tacites) et la logique formelle (interprétée sous la théorie des types dépendants). Les métriques d'évaluation standard — telles que les scores BLEU par rapport à une référence, les vérifications ponctuelles par des experts ou le succès de la preuve en aval — ne parviennent pas à détecter les échecs « insidieux » où la formalisation est fluide et prouvable, mais sémantiquement erronée.

Le papier formalise ce problème via une distribution d'interprétation ($D_N$), représentant l'ensemble des énoncés formels qu'un mathématicien compétent accepterait comme exprimant un énoncé $N$ donné en LN. Un candidat de formalisation $F$ est $\epsilon$-fidèle s'il est prouvablement équivalent à $1-\epsilon$ des énoncés dans $D_N$. Les auteurs catégorisent la dérive sémantique en quatre classes canoniques :

1. $\Delta\forall$ (Inversion de quantificateur) : Inversion de l'ordre des quantificateurs (ex: $\forall x \exists y$ vs $\exists y \forall x$).
2. $\Delta H$ (Omission d'hypothèse) : Suppression d'une prémisse, rendant l'énoncé formel strictement plus fort que prévu.
3. $\Delta C$ (Généralisation de la conclusion) : Renforcement de la conclusion telle que $F \Rightarrow N$ mais $N \not\Rightarrow F$.
4. $\Delta T$ (Coercition de type) : Réétiquetage silencieux des types (ex: $\mathbb{R} \to \mathbb{Q}$), souvent le plus difficile à détecter syntaxiquement.

2. Méthodologie : Empreinte de prouvabilité bidirectionnelle (BPF)

La contribution centrale est l'Empreinte de prouvabilité bidirectionnelle (Bidirectional Provability Fingerprinting - BPF), un cadre sans référence qui certifie la fidélité en comparant les « voisinages de conséquence » de l'énoncé en LN et du candidat formalisé.

2.1. Le mécanisme central

Le BPF repose sur l'idée qu'le sens d'un énoncé est défini par ce qu'il implique et par ce qui l'implique.

• Empreinte directe ($\Phi^+_F$) : L'ensemble des sondes impliquées par le candidat $F$.
• Empreinte inverse ($\Phi^-_F$) : L'ensemble des sondes qui impliquent $F$.
• Équivalence : Deux énoncés sont sémantiquement équivalents si leurs empreintes directe et inverse coïncident sur un ensemble de sondes suffisamment riche.

Le pipeline comprend :

1. Génération de sondes : Synthèse d'un ensemble de sondes sémantiques ($P$) à partir de l'énoncé $N$ en LN.
2. Autoformalisation : Conversion de ces sondes en énoncés formels.
3. Vérification d'implication : Utilisation d'un assistant de preuve (Lean 4 + mathlib4) comme oracle pour calculer les relations d'implication entre $F$ et les sondes.
4. Comparaison d'empreintes : Comparaison de l'empreinte du candidat avec l'empreinte prédite dérivée de $N$.

2.2. Composants clés

Le cadre introduit quatre composants novateurs pour améliorer la détection et l'efficacité :

1. Génération de sondes contrefactuelles (CPG) :
   Au lieu d'un échantillonnage générique, la CPG utilise une procédure contrastive. Elle génère mécaniquement des « jumeaux déviés » ($N^D$) pour chacune des quatre classes de dérive (par exemple, en inversant les quantificateurs). Un LLM est ensuite incité à générer des sondes qui distinguent spécifiquement $N$ de $N^D$. Cela cible les modes de défaillance spécifiques que le certificateur vise à détecter.

2. Le spectre d'équivalence ($E(F, N)$) :
   Remplaçant les verdicts binaires fragiles (Fidèle/Dévié) par un score continu dans $[0, 1]$. Ce score est calibré par rapport à des annotations d'experts pour définir trois régions de décision :

   • ACCEPT (ACCEPTER) : $E \ge 0,93$
   • REVIEW (RÉVISER) : $0,78 \le E < 0,93$ (nécessite un tri humain)
   • REJECT (REJETER) : $E < 0,78$

3. Allocation adaptative du budget de sondage (APBA) :
   Un routeur informationnel qui alloue dynamiquement le « budget de tactique » (temps/coût de recherche de preuve) limité. L'APBA sélectionne les sondes qui maximisent la réduction attendue de l'entropie concernant l'état de dérive, plutôt que de procéder par échantillonnage uniforme. Cela permet d'atteindre le même taux de détection avec nettement moins de sondes.

4. Décodage guidé par la fidélité (FGD) :
   Une boucle de rétroaction où les scores BPF sont utilisés comme signal de récompense pendant le processus d'autoformalisation. Dans une configuration de échantillonnage et de reclassement (sample-and-rerank), les candidats sont scorés par le BPF. Si les meilleurs candidats tombent dans les zones « REVIEW » ou « REJECT », le « témoin de sonde » le plus élevé (la sonde spécifique qui a révélé la dérive) est renvoyé au LLM comme indice contextuel pour réparer l'erreur.

3. Garanties théoriques

Le papier fournit deux résultats théoriques principaux :

• Théorème de détection de dérive : Prouve que pour toute classe de dérive $D$ spécifique, si le générateur de sondes possède un « taux de témoignage » non nul ($\alpha$), le BPF peut détecter la dérive avec une probabilité de $1-\delta$ en utilisant un budget de sondes $k \ge \frac{1}{\alpha} \log(1/\delta)$.
• PAC-Fidélité : Établit que la classe d'équivalence d'un énoncé en LN est apprenable à partir de $O(\log(1/\delta)/\epsilon)$ sondes, en supposant que la distribution des sondes peut témoigner de toute dérive atteignable.

Les auteurs reconnaissent également des limites : le BPF ne peut pas détecter la dérive de convention (où la notation change mais le contenu logique reste identique) et dépend de la complétude de l'oracle de preuve (des preuves incomplètes peuvent conduire à des faux négatifs).

4. Résultats expérimentaux

Les auteurs ont publié DRIFTBENCH, un benchmark de 2 183 paires LN/Lean 4 avec des étiquettes de dérive contrôlées à travers six sous-domaines mathématiques.

Performance de détection :

• BPF + CPG détecte 89,6 % des formalisations déviées avec un taux de faux positifs de 3,0 %.
• Cela surpasse largement les bases de référence :
  • Vérification de type uniquement : 11,4 % de détection.
  • Prouvabilité (indicateur d'impossibilité de preuve) : 41,2 % de détection.
  • LLM-judge (vérification directe de la fidélité) : 63,3 % de détection.
  • Back-translation (rétro-traduction) : 58,9 % de détection.
• APBA réduit le coût computationnel (temps de calcul) de 3,2× par rapport à l'échantillonnage uniforme tout en maintenant les taux de détection.

Impact du FGD :
Appliqué comme étape de post-traitement à un autoformaliseur de pointe, le FGD a réduit le taux d'énoncés déviés émis de 19,4 % à 10,3 % (une réduction relative de 47 %), principalement en re-promptant sur les erreurs d'omission d'hypothèse et de généralisation de conclusion.

5. Signification et revendications

Le papier affirme que le fossé de fidélité est le principal goulot d'étranglement pour une autoformalisation fiable à l'échelle de bibliothèques mathématiques complètes. La signification de ce travail réside dans :

1. Certification sans référence : Il fournit une méthode pour vérifier la fidélité sans nécessiter de formalisation « de référence », qui est souvent indisponible.
2. Opérationnalisation de la sémantique : Il déplace le paradigme d'évaluation de la superposition syntaxique (BLEU) ou de la prouvabilité vers la sémantique inférentielle (voisinages de conséquence), s'alignant ainsi sur la sémantique de la théorie des preuves.
3. Scalabilité : En introduisant l'APBA et le spectre d'équivalence, il offre un outil de triage pratique et rentable qui permet de prioriser la revue par des experts humains plutôt que de la remplacer.
4. Benchmarking : DRIFTBENCH est présenté comme le premier benchmark avec des étiquettes de dérive contrôlées, permettant une évaluation systématique de la fidélité plutôt que de la simple capacité de preuve.

Les auteurs positionnent le BPF non pas comme une solution parfaite éliminant tous les erreurs (notant spécifiquement la limite concernant la dérive de convention), mais comme une étape concrète vers la fermeture du fossé de fidélité, permettant l'intégration sûre des mathématiques générées par IA dans des bibliothèques rigoureuses.