A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

Cette étude propose une approche neuro-symbolique combinant la génération par des modèles de langage, la récupération de problèmes analogues et la vérification formelle pour améliorer significativement la fiabilité et la précision de la génération de preuves en géométrie euclidienne.

L'essentiel

Imaginez que vous essayez d'enseigner à un génie très créatif mais un peu étourdi comment résoudre des énigmes de géométrie. Ce "génie", c'est une Intelligence Artificielle (un grand modèle de langage comme ceux qui écrivent des textes). Le problème ? Ce génie est excellent pour imiter le style d'une réponse, mais il est souvent mauvais pour la logique stricte nécessaire aux preuves mathématiques. Il a tendance à inventer des choses qui semblent vraies, mais qui ne le sont pas.

Les auteurs de cette recherche ont créé une méthode intelligente, qu'ils appellent une approche "Neuro-Symbolique". Pour faire simple, c'est comme donner à ce génie étourdi deux super-pouvoirs pour l'aider à ne plus se tromper.

Voici comment cela fonctionne, expliqué avec des analogies simples :

1. Le Problème : Le Génie qui "Hallucine"

Les modèles d'IA actuels fonctionnent un peu comme un acteur qui improvise. Si on lui demande de prouver un théorème de géométrie, il va essayer de deviner la suite logique en se basant sur ce qu'il a lu dans des millions de livres. Mais en mathématiques, il n'y a pas de place pour l'improvisation : chaque étape doit être 100 % vraie. Sinon, toute la preuve s'effondre.

2. La Solution : Le Duo "Guide + Vérificateur"

L'équipe a conçu un système en deux étapes pour aider l'IA :

Étape A : Le "Guide" (L'Analogie)

Imaginez que vous devez résoudre un casse-tête complexe. Au lieu de commencer de zéro, vous regardez un puzzle similaire que vous avez déjà résolu hier. Vous vous dites : "Ah, pour celui-là, j'avais utilisé cette pièce ici, et cette autre là-bas."

C'est exactement ce que fait le système :

• Il cherche dans sa base de données des problèmes de géométrie qui ressemblent structurellement à celui qu'il doit résoudre (même si les noms des points ou les chiffres sont différents).
• Il montre à l'IA la solution de ce problème similaire.
• L'analogie : C'est comme donner à un étudiant un exemple de devoir corrigé avant de lui donner le sien. Cela l'aide à comprendre la "méthode" plutôt que de deviner au hasard.
• Le bonus : Cela permet aussi de ne montrer à l'IA que les règles (théorèmes) utiles pour ce cas précis, au lieu de lui donner tout un dictionnaire de 18 000 pages. C'est plus rapide et moins cher !

Étape B : Le "Vérificateur" (Le Contrôleur)

Même avec un guide, l'IA peut encore faire une erreur. C'est là qu'intervient le deuxième super-pouvoir : un vérificateur automatique.

• Imaginez un professeur de mathématiques très strict et infatigable qui ne dort jamais.
• Dès que l'IA propose une preuve, ce professeur la lit ligne par ligne.
• S'il trouve une erreur (par exemple, "Tu as utilisé cette règle alors que la condition n'était pas remplie"), il ne rejette pas tout le travail. Il renvoie la copie à l'IA en disant : "Regarde, erreur à la ligne 3. Corrige-la et réessaie."
• L'IA corrige, renvoie, et le professeur vérifie à nouveau. Ce cycle continue jusqu'à ce que la preuve soit parfaite.

3. Les Résultats : Une Révolution de la Fiabilité

Les auteurs ont testé cette méthode sur des problèmes de géométrie de niveau examen (SAT). Les résultats sont impressionnants :

• Sans aide, les IA les plus avancées (comme o1 ou Gemini) réussissaient à peine 10 % des preuves complexes.
• Avec ce système de Guide + Vérificateur, le taux de réussite a explosé, atteignant jusqu'à 80 % !

C'est comme si on prenait un élève moyen et qu'on lui donnait un tuteur personnel et un correcteur automatique : il passe de "je ne comprends rien" à "je suis excellent".

Pourquoi est-ce important ?

Aujourd'hui, on utilise de plus en plus l'IA pour des tâches critiques (médecine, ingénierie, sécurité). Si l'IA invente une preuve mathématique fausse, cela peut être dangereux.
Cette méthode montre qu'on peut rendre l'IA fiable. En combinant la créativité de l'IA (qui sait écrire et proposer des idées) avec la rigueur de la logique symbolique (qui vérifie les faits), on ouvre la porte à des applications où l'on peut vraiment faire confiance à la machine.

En résumé :
Les chercheurs ont appris à l'IA à ne pas travailler seule. Ils lui donnent un modèle à copier (l'analogie) pour bien démarrer, et un professeur sévère (le vérificateur) pour corriger ses erreurs jusqu'à ce que tout soit parfait. C'est une recette simple mais puissante pour transformer des "rêveurs" en "mathématiciens fiables".

Résumé technique

Voici un résumé technique détaillé de l'article « A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry » (Une approche neuro-symbolique pour la génération de preuves fiables avec les LLM : Étude de cas en géométrie euclidienne).

1. Problématique

Les grands modèles de langage (LLM) excellent dans la génération de texte naturel mais éprouvent de grandes difficultés dans les domaines formels exigeant une déduction logique rigoureuse et un raisonnement symbolique, tels que la génération de preuves mathématiques.

• Limites actuelles : L'architecture des LLM repose sur la génération de séquences probabilistes basées sur des corrélations statistiques plutôt que sur une compréhension logique profonde. Ils manquent souvent de cohérence logique sur de longues chaînes de raisonnement et commettent des erreurs de syntaxe ou de prémisse dans les preuves formelles.
• Objectif : Développer un système capable de guider les LLM pour générer des preuves mathématiques vérifiables, fiables et exactes, en particulier dans le domaine de la géométrie euclidienne (niveau SAT).

2. Méthodologie : Une Approche Neuro-Symbolique

Les auteurs proposent une architecture hybride combinant la puissance générative des LLM avec deux composants structurés : l'orientation par analogie et la vérification symbolique. Le système fonctionne selon un pipeline itératif (illustré dans la Figure 1 de l'article) :

A. Abstraction et Recherche d'Analogies (Guidage)

1. Abstraction du problème : Les problèmes géométriques (construction, conditions, objectif) sont abstraits en remplaçant les noms d'entités et les valeurs numériques par des placeholders (ex: <word>, <num>). Cela permet de capturer la structure sous-jacente indépendamment des détails de surface.
2. Récupération d'analogues : Un régresseur (réseau de neurones simple) est entraîné pour prédire la similarité de preuve entre deux problèmes abstraits en utilisant la similarité de Jaccard sur les ensembles de constructions et de conditions.
3. Sélection de théorèmes : Au lieu de fournir tout le dictionnaire de théorèmes (196 théorèmes), le système extrait uniquement les théorèmes utilisés dans les preuves des problèmes analogues récupérés. Cela réduit considérablement la taille du contexte (de 18k à ~2,5k tokens en moyenne) et guide le modèle vers les outils pertinents.

B. Génération de Preuve par le LLM

Le LLM reçoit :

• Le problème cible (texte et représentation formelle).
• Des exemples few-shot : les problèmes analogues récupérés avec leurs preuves formelles complètes.
• Le dictionnaire de théorèmes restreint.
• La tâche : générer une preuve formelle étape par étape en utilisant uniquement les théorèmes fournis.

C. Vérificateur Symbolique et Boucle de Feedback

Un vérificateur externe, basé sur la logique formelle et le solveur SMT Z3, évalue la preuve générée :

• Fonctionnement : Il encode les étapes de la preuve et les contraintes géométriques sous forme de formules logiques. Il ne connaît pas la solution par cœur ; il vérifie si la conclusion est déduite logiquement des prémisses.
• Feedback itératif : Si la preuve est incorrecte, le vérificateur identifie la première erreur et fournit un retour structuré au LLM pour une nouvelle tentative.
• Catégories d'erreurs :
  1. Violation de syntaxe : Théorèmes non définis ou signatures d'arguments incorrectes.
  2. Violation de prémisse : Utilisation d'un théorème dont les conditions préalables n'ont pas été dérivées.
  3. Objectif non atteint : La preuve est syntaxiquement correcte mais ne mène pas à la conclusion souhaitée.

3. Contributions Clés

1. Système Neuro-Symbolique : Intégration réussie de l'orientation par analogie et de la vérification formelle pour améliorer la génération de preuves par des LLM généraux.
2. Vérificateur Expressif : Conception d'un vérificateur capable d'évaluer l'intégralité d'une preuve (et pas seulement la réponse numérique) et de fournir un feedback hiérarchisé pour corriger les erreurs.
3. Réduction des Coûts et du Bruit : Utilisation de la récupération d'analogies pour filtrer le dictionnaire de théorèmes, réduisant la taille du contexte et améliorant la focalisation du modèle.
4. Validation Empirique : Démonstration que cette approche fonctionne sur plusieurs familles de modèles (OpenAI o1 et Gemini-2.5-Flash) sans nécessiter de réentraînement (fine-tuning).

4. Résultats Expérimentaux

Les expériences ont été menées sur le jeu de données FormalGeo-7k (6 981 problèmes de géométrie euclidienne de niveau SAT).

• Performance Globale :
  • Le pipeline complet (analogie + vérificateur + multiples tentatives) atteint une précision moyenne de 80 %.
  • Comparé au modèle de base (o1) sans ces améliorations (10 % de précision), cela représente un gain de 58 % à 70 %.
  • Pour Gemini-2.5-Flash, les gains sont de 52 % à 64 % (passant de 22 % à 86 % avec le pipeline complet).
• Analyse par Composant :
  • Récupération d'analogies : Améliore la précision initiale de 10 % à 48 % (sur o1, sans vérificateur).
  • Feedback du vérificateur : Ajoute environ 20 % de gain supplémentaire en permettant des itérations de correction.
  • Multiples exécutions : Permet de résoudre les problèmes les plus difficiles (niveaux 4-5) où la première tentative échoue souvent.
• Efficacité : Le système nécessite moins de tentatives (retries) et de runs que le modèle de base pour atteindre une solution correcte.
• Précision de la preuve vs Réponse : Le modèle de base trouve souvent la bonne réponse numérique (90 %) mais échoue à fournir la preuve correcte (57,7 %). La méthode proposée atteint 100 % de réponses correctes et 80 % de preuves correctes, comblant le fossé entre l'intuition et la justification formelle.

5. Signification et Perspectives

• Fiabilité des LLM : Cette étude démontre que les LLM peuvent être rendus fiables pour des tâches critiques nécessitant une vérité absolue (mathématiques, sécurité) en les couplant à des outils symboliques.
• Généralisation : Bien que testé en géométrie, l'approche est conçue pour être adaptable à d'autres domaines formels supportant la vérification SMT.
• Applications Éducatives : Le système pourrait servir d'outil pédagogique, fournissant des problèmes analogues pour guider les étudiants et un vérificateur pour offrir un feedback ciblé.
• Limitations : L'approche dépend actuellement de la capacité du vérificateur Z3 (manque de support pour les fonctions trigonométriques inverses) et ne prend pas en compte les diagrammes visuels (bien que les LLM multimodaux aient montré des difficultés avec les aspects visuels des problèmes mathématiques).

En conclusion, cette recherche propose une feuille de route scalable pour construire des systèmes d'IA robustes dans les domaines STEM, en combinant la flexibilité des modèles de langage avec la rigueur du raisonnement formel.