Résumé Technique : Amélioration de l'Autoformalisation en Lean4 par Affinage Fin avec Cohérence Cyclique

1. Problématique

L'autoformalisation consiste à traduire automatiquement des énoncés mathématiques en langage naturel (NL) vers un langage de preuve formel, tel que Lean4. Bien que les grands modèles de langage (LLM) aient fait des progrès significatifs en raisonnement mathématique, cette tâche reste difficile. Les modèles tendent souvent à produire du code Lean4 syntaxiquement valide (qui compile) mais sémantiquement incorrect, ne capturant pas le sens mathématique réel de l'énoncé.

Le défi principal réside dans l'évaluation de la qualité sémantique de la traduction sans recourir à un vérificateur de preuves complet (qui est coûteux en temps de calcul) ou à une annotation humaine massive.

2. Méthodologie

L'auteur aborde ce problème comme une tâche de séquence-à-séquence et propose un pipeline d'entraînement combinant l'apprentissage supervisé (SFT) et l'apprentissage par renforcement (RL).

2.1. Architecture et Modèles

• Modèle de base : Utilisation de Qwen3.5-2B (2 milliards de paramètres).
• Fine-tuning : Application de LoRA (Low-Rank Adaptation) restreinte aux sous-couches feed-forward (FFN) pour limiter les paramètres entraînables à environ 9,4 millions, rendant l'entraînement possible sur un seul GPU.
• Deux modèles :
  1. $f_\theta$ : Traducteur NL $\to$ Lean4 (entraîné).
  2. $g_\phi$ : Traducteur Lean4 $\to$ NL (traducteur de retour, "back-translator", figé après le SFT).

2.2. Données

• Ensemble d'entraînement : FineLeanCorpus (FLC), contenant 509 000 paires NL/Lean4 avec des notes de difficulté (1 à 10).
• Nettoyage : Suppression des doublons, des erreurs de compilation et décontamination stricte par rapport à PutnamBench (benchmark de 660 problèmes de compétition) pour éviter le surapprentissage.
• Évaluation : Un sous-ensemble maintenu de FLC (700 exemples) et PutnamBench.

2.3. Stratégies d'Entraînement Comparées

L'étude compare trois régimes d'entraînement :

1. SFT avec Curriculum : Entraînement séquentiel par difficulté croissante (1 $\to$ 10).
2. SFT sans Curriculum : Entraînement sur l'ensemble des données mélangées (shuffled).
3. RL par GRPO (Group Relative Policy Optimization) :
   • Le modèle est initialisé à partir du checkpoint SFT.
   • Récompense : Basée sur la cohérence cyclique. Pour un énoncé $s$, le modèle génère une formalisation $\hat{l}$, qui est re-traduite en NL ($\hat{s}'$) par $g_\phi$. La récompense est la similarité cosinus entre les embeddings de $s$ et $\hat{s}'$.
   • Cela permet d'optimiser la fidélité sémantique du cycle $NL \to Lean4 \to NL'$ sans utiliser de vérificateur de preuves externe.

3. Contributions Clés

1. Pipeline d'autoformalisation efficace : Mise en œuvre d'un pipeline LoRA sur Qwen3.5-2B avec une décontamination rigoureuse des données.
2. Étude d'ablation du Curriculum : Démonstration que l'ordre des difficultés (curriculum learning) n'apporte aucun bénéfice mesurable par rapport à un entraînement mélangé pour cette échelle de modèle (2B) et de données.
3. RL avec récompense de cohérence cyclique : Introduction d'une méthode GRPO utilisant la similarité sémantique (embeddings) comme signal de récompense. Cette approche surpasse significativement le SFT tout en maintenant une faible dégradation de la capacité de modélisation du langage (perte d'entropie croisée).

4. Résultats

Les résultats sont présentés dans le Tableau 1 et les Figures du papier.

4.1. Performance (Cohérence Cyclique Moyenne)

La métrique principale est la similarité cosinus moyenne ($\bar{C}$) entre l'énoncé original et la re-traduction.

• Sur FLC (Hold-out) :
  • SFT (Curriculum) : 0.513
  • SFT (Sans Curriculum) : 0.519
  • RL (GRPO) : 0.669 (Amélioration de +0.156 par rapport au SFT).
• Sur PutnamBench (Problèmes plus difficiles) :
  • SFT (Curriculum) : 0.422
  • RL (GRPO) : 0.561 (Amélioration de +0.139).

4.2. Analyse Statistique et Coûts

• Significativité : Les améliorations du RL sont statistiquement significatives ($p < 10^{-56}$).
• Impact sur la qualité linguistique : L'augmentation de la perte d'entropie croisée (Cross-Entropy) est minime (+0.011 nats), indiquant que le modèle n'a pas perdu sa capacité de base à générer du texte cohérent.
• Comparaison d'échelle : Un modèle 9B entraîné uniquement en SFT (0.585 sur FLC) est inférieur au modèle 2B entraîné en RL (0.669), montrant que le signal RL est plus efficace que l'augmentation de la taille du modèle pour cette tâche spécifique sur des données en distribution.

4.3. Observations par Domaine

• Les domaines algébriques et de théorie des nombres bénéficient le plus du RL (scores > 0.72 sur FLC).
• Les domaines continus (calcul, analyse) obtiennent des scores plus faibles, probablement en raison de la complexité structurelle des définitions $\epsilon$-$\delta$ en Lean4, ce qui rend la re-traduction plus bruyante.

5. Signification et Limites

Signification

Ce travail démontre que la cohérence cyclique est un signal d'apprentissage robuste pour l'autoformalisation mathématique. Elle permet d'optimiser la fidélité sémantique sans nécessiter de compilateur Lean4 en temps réel ou de vérificateur de preuves, réduisant ainsi considérablement la latence et le coût de calcul. De plus, l'échec du curriculum learning suggère que pour les modèles de taille moyenne, la diversité des données (via le mélange) est plus importante que l'ordre de difficulté.

Limites et Avertissements

1. Biais du traducteur de retour : La métrique dépend d'un modèle $g_\phi$ figé. Si ce modèle a des biais systématiques, tous les modèles évalués seront affectés de la même manière.
2. Hacking de récompense (Reward Hacking) : L'analyse qualitative révèle des cas où le modèle génère du code Lean4 qui ressemble trop au langage naturel, permettant au traducteur de retour de "recopier" l'entrée originale, obtenant ainsi une récompense parfaite (1.0) sans véritable compréhension sémantique.
3. Validité mathématique : La cohérence cyclique mesure la fidélité de la traduction, mais pas la vérité mathématique. Un énoncé formel peut être cohérent avec l'original mais mathématiquement faux (bien que le papier note que l'utilisation de sorry comme placeholder empêche la vérification de la preuve).

Perspectives Futures

L'auteur suggère d'intégrer le feedback du compilateur Lean4 comme une récompense "dure" (hard reward) en complément du signal de cohérence cyclique "doux" (soft reward), et d'explorer des métriques d'équivalence sémantique plus robustes que les simples embeddings de phrases.