🤖 AI

HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

Le document présente Hermes, un nouvel agent assisté par des outils qui entrelace le raisonnement informel avec des preuves formellement vérifiées dans Lean afin d'obtenir un raisonnement mathématique plus précis, efficace et vérifiable dans les grands modèles de langage par rapport aux approches existantes.

Auteurs originaux : Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, Farzan Farnia

Publié 2026-06-01

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, Farzan Farnia

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

Imaginez que vous essayez de résoudre une énigme mathématique très difficile. Vous avez un assistant brillant mais légèrement éparpillé (le Large Language Model, ou LLM) qui est excellent pour le brainstorming d'idées et pour rédiger de longues explications créatives. Cependant, cet assistant fait parfois de petites erreurs logiques, s'embrouille ou « hallucine » des faits qui semblent vrais mais ne le sont pas.

D'un autre côté, vous avez un Juge Mathématique strict et inflexible (un système de preuve formel appelé Lean). Ce juge ne fait jamais d'erreurs, mais il est très rigide. Il ne comprend pas votre brainstorming créatif ; il n'accepte que du code parfaitement structuré et formel. Si vous lui donnez une explication désordonnée, il répond simplement « Erreur ».

Hermes est un nouvel outil qui agit comme un traducteur et un gestionnaire de contrôle qualité entre ces deux entités. Il laisse votre assistant créatif travailler librement, mais l'arrête toutes les quelques étapes pour demander au Juge strict : « Cette étape spécifique est-elle réellement vraie ? »

Voici comment fonctionne Hermes, décomposé en parties simples :

1. Le Problème : La « Longue Marche » contre l'« Examen Strict »

L'ancienne méthode (Raisonnement informel) : Votre assistant essaie de résoudre tout le problème en un seul long flux de pensée. C'est flexible et rapide, mais s'il prend un mauvais tournant tôt dans le processus, il peut continuer à marcher dans la mauvaise direction pendant longtemps avant de réaliser son erreur. C'est comme conduire une voiture les yeux fermés, en espérant ne pas heurter un mur.
L'autre méthode (Preuve formelle) : Votre assistant essaie d'écrire la solution en code strict dès le début. C'est parfaitement précis, mais c'est si lent et difficile que l'assistant finit souvent par se bloquer ou abandonner. C'est comme essayer de construire une maison brique par brique en vérifiant chaque brique par rapport à un plan avant d'en poser la suivante.

2. La Solution Hermes : Le système de « Points de Contrôle »

Hermes combine le meilleur des deux mondes. Il laisse l'assistant rédiger quelques étapes de son explication créative, puis effectue une pause pour lancer un « point de contrôle ».

Le Traducteur (Module de Formalisation) : Quand l'assistant dit : « Par conséquent, l'angle est de 45 degrés », Hermes traduit cette phrase en le code strict que le Juge comprend.
Le Juge (Module de Preuve) : Le Juge strict vérifie ce code.
- Si cela passe : Super ! Hermes enregistre cette étape dans une Banque de Mémoire et dit à l'assistant : « C'est bon, continue. »
- Si cela échoue : Le Juge dit : « Non, c'est faux. » Hermes dit à l'assistant : « Stop ! Tu as fait une erreur ici. Reviens en arrière et corrige-la. »
La Banque de Mémoire : Parce que les problèmes mathématiques impliquent souvent de longues chaînes de logique, Hermes se souvient de toutes les étapes qui ont été validées. Cela garantit que l'assistant n'oublie pas les règles qu'il a déjà prouvées, maintenant ainsi la cohérence de l'ensemble de l'argument.

3. Pourquoi est-ce meilleur ? (Les Résultats)

L'article a testé Hermes sur des compétitions mathématiques difficiles (comme l'AIME et HARDMath2) en utilisant divers modèles d'IA.

Précision : Hermes a rendu l'IA beaucoup plus intelligente. Sur les problèmes les plus difficiles, il a amélioré le taux de réussite de l'IA jusqu'à 40 %. Il a empêché l'IA de donner des réponses erronées avec assurance.
Efficacité : Vous pourriez penser que vérifier chaque étape serait lent et coûteux. Étonnamment, Hermes était en fait plus rapide et moins coûteux (en termes de puissance de calcul) que d'autres méthodes qui tentent de générer 5 ou 10 réponses différentes pour choisir la meilleure. C'est comme prendre un chemin direct et vérifié plutôt que de errer dans un labyrinthe en essayant 10 routes différentes.
Clarté : Contrairement à d'autres méthodes qui disent simplement « Cette réponse a 80 % de chances d'être correcte », Hermes donne un « Oui » ou un « Non » clair sur des étapes spécifiques, ce qui permet de comprendre plus facilement pourquoi une réponse est correcte ou fausse.

L'essentiel

Hermes est comme si vous donniez à votre assistant mathématique créatif un éditeur intelligent et automatisé qui vérifie son travail en temps réel. Cela ne l'empêche pas de penser de manière créative ; cela l'empêche simplement de tomber d'une falaise. Le résultat est une IA de résolution mathématique qui est non seulement plus précise, mais aussi plus efficace et plus facile à faire confiance.

Résumé Technique : HERMES – Vers un raisonnement mathématique efficace et vérifiable dans les LLM

1. Énoncé du problème

Les grands modèles de langage (LLM) ont démontré une compétence significative en raisonnement mathématique via des méthodes informelles comme la Chaîne de Pensée (Chain-of-Thought, CoT). Cependant, le raisonnement purement informel est sujet aux lacunes logiques, aux erreurs subtiles et aux hallucinations, particulièrement dans les chaînes de raisonnement longues. Les systèmes de preuve de théorèmes formels (ex. Lean4, Coq) offrent un raisonnement rigoureux et vérifiable par machine, mais manquent souvent de la flexibilité exploratoire et de l'expressivité de la résolution de problèmes en langage naturel. Les approches actuelles tentant de combler ce fossé, telles que les Modèles de Récompense de Processus (PRM) et les Modèles de Récompense de Résultat (ORM), reposent sur des évaluateurs "boîte noire" qui attribuent des scores numériques sans vérification explicite de la correction mathématique. De plus, ces méthodes basées sur la récompense nécessitent souvent une importante curation humaine et peuvent hériter de la stochasticité et des biais des LLM utilisés comme évaluateurs, menant à un désalignement avec la véritable exactitude étape par étape.

Le défi central abordé par ce travail est l'absence d'un mécanisme principiel permettant aux agents mathématiques basés sur les LLM de combiner la flexibilité du raisonnement informel avec la vérifiabilité des preuves formelles, de manière à la fois efficace et interprétable.

2. Méthodologie : Le cadre Hermes

Les auteurs introduisent Hermes (Hybrid AgEnt for Reasoning in Mathematics with NEuro-Symbolic Lean4 verification), un agent multi-modulaire assisté par outils, conçu pour entrelacer le raisonnement informel avec des preuves formellement vérifiées dans Lean4. Le cadre fonctionne via un processus d'inférence itératif impliquant quatre modules clés :

LLM de Raisonnement : Génère des étapes de raisonnement en langage naturel. Le modèle est instruit de vérifier chaque étape mathématique critique contribuant à la preuve finale.
Module de Formalisation : Traduit l'étape de preuve en langage naturel en une déclaration Lean4 correspondante. Pour garantir la fidélité sémantique, ce module emploie un processus de vérification en deux étapes :
1. Vérification de Compilation : Le code Lean généré doit compiler avec succès.
2. Rétro-traduction : Le code Lean compilé est rétro-traduit en langage naturel. Le LLM évalue l'équivalence entre l'étape originale et la version rétro-traduite.
  Ce processus est répété jusqu'à un budget $K_f$ pour assurer une formalisation valide.
Module de Preuve (Prover) : Reçoit la déclaration Lean validée et tente de prouver l'objectif ou sa négation ( $\neg \text{objectif}$ ) en utilisant une combinaison d'un modèle de génération de preuve complète (ex. Goedel-Prover-V2) et de solveurs Lean intégrés. Ce module opère sous un budget d'échantillonnage $K_p$ . Il retourne un signal binaire : CORRECT (preuve trouvée), INCORRECT (contre-preuve trouvée), ou ÉCHEC DE VÉRIFICATION (incapable de prouver ou de disprover).
Bloc de Mémoire : Une base de données structurée qui stocke les étapes de preuve validées ainsi que leurs représentations vectorielles. Elle utilise un mécanisme de récupération top- $k$ pour injecter un contexte pertinent et précédemment vérifié dans l'étape de raisonnement actuelle, assurant la continuité et empêchant la propagation d'erreurs dans les longues chaînes de raisonnement.

Boucle de Rétroaction : Selon le signal du prouveur, le LLM poursuit soit le chemin de raisonnement actuel (si vérifié), soit révise l'étape (si une contre-preuve est trouvée), soit explore des approches alternatives. Le système est conçu pour être modulaire, permettant aux composants comme l'auto-formaliseur ou le prouveur d'être remplacés à mesure qu'ils progressent.

Analyse de Complexité : Les auteurs fournissent une analyse théorique de la complexité d'inférence au niveau du jeton (token). Ils soutiennent que Hermes, qui entrelace la vérification lors de l'inférence sur un sous-ensemble d'étapes critiques, possède une complexité de $O(\tilde{T} K N^2)$ , où $\tilde{T}$ est le nombre d'étapes vérifiées. Cette complexité est théoriquement bornée par la complexité des méthodes basées sur les PRM ( $O(T K N^2)$ ) et est nettement plus efficace que la génération de multiples traces complètes pour la sélection "Best-of-N".

3. Contributions Clés

L'article revendique les contributions primaires suivantes :

Premier Agent basé sur l'outil Lean4 : Hermes est présenté comme le premier agent basé sur des outils qui vérifie les étapes de preuve intermédiaires réalisables pendant l'inférence, fournissant aux LLM des signaux de correction basés sur le noyau (kernel) dérivés d'un compilateur de confiance plutôt que d'un modèle de récompense appris.
Mémoire pilotée par Lean4 : L'introduction d'un bloc de mémoire qui accumule et valide les affirmations intermédiaires en contexte, assurant la cohérence entre les étapes et réduisant la propagation d'erreurs dans les longues chaînes de raisonnement.
Gains d'Efficacité et de Précision : Des preuves empiriques démontrant que Hermes améliore la précision du raisonnement tout en réduisant considérablement l'utilisation de jetons et le coût computationnel par rapport aux approches basées sur la récompense.

4. Résultats Expérimentaux

Le cadre a été évalué sur quatre benchmarks de raisonnement mathématique exigeants : MATH-500, AIME'25, CollegeMath, et HARDMath2, en utilisant des LLM de différentes échelles (Qwen3-8B, OpenAI o3-mini, DeepSeek-V3.1/V3.2).

Améliorations de la Précision : Dans tous les réglages, Hermes a systématiquement surpassé le Zero-shot CoT, le Majority Vote, et divers modèles de récompense de base (ORM et PRM).
- En moyenne, Hermes a amélioré la précision de 23 % sur les quatre benchmarks.
- Sur le jeu de données difficile AIME'25, Hermes a obtenu une amélioration de la précision de 40 % par rapport au modèle de base (ex. DeepSeek-V3.2) tout en utilisant 80 % de FLOPs d'inférence en moins que les méthodes basées sur la récompense.
- Lorsqu'il est mis à l'échelle au moment du test (Hermes@5 avec échantillonnage Best-of-N), la précision s'améliore encore de 20 %.
Efficacité : Hermes a utilisé nettement moins de jetons que les méthodes basées sur le score (Safe, ORM, PRM). Alors que les méthodes basées sur la récompense nécessitaient souvent de générer 5 à 60 traces de raisonnement pour atteindre une précision compétitive, Hermes a obtenu des résultats supérieurs avec une seule trace (@1) ou un échantillonnage minimal, réduisant les budgets de jetons de 4 à 6 fois.
Études d'Ablation : Le retrait du module de Preuve (Prover) a causé la plus forte chute de performance (ex. une baisse relative de 25 % sur AIME), soulignant la nécessité du moteur de recherche de preuve. Le retrait du tampon de Mémoire a perturbé la continuité du raisonnement, particulièrement sur les jeux de données plus difficiles avec des chaînes de raisonnement plus longues.
Sensibilité au Domaine : Les gains de performance ont été plus prononcés sur les jeux de données difficiles (HARDMath2, AIME) par rapport aux plus faciles (MATH-500), suggérant que Hermes est particulièrement efficace pour corriger les erreurs dans le raisonnement avancé. Le système a montré de solides performances en algèbre et équations (où Mathlib est dense) et des gains légèrement inférieurs en géométrie, attribués à l'état actuel de la bibliothèque formelle.

5. Signification et Revendications

Les auteurs positionnent Hermes comme une étape significative vers l'unification du raisonnement mathématique informel et formel. Ils affirment qu'en intégrant la vérification formelle directement dans la boucle de raisonnement, le cadre offre :

Interprétabilité : Contrairement aux modèles de récompense "boîte noire", Hermes fournit un feedback explicite de correction au niveau de l'étape, révélant pourquoi un chemin de raisonnement est valide ou défectueux.
Évolutivité et Modularité : La conception permet l'intégration transparente d'auto-formaliseurs et de prouveurs améliorés à mesure que le domaine progresse, garantissant que le système reste pertinent au-delà des capacités actuelles de Lean4.
Efficacité des Ressources : Ce travail démontre qu'un raisonnement mathématique de haute qualité ne nécessite pas nécessairement des budgets computationnels massifs associés à la génération de milliers de traces candidates ; au contraire, des vérifications intermédiaires ciblées et vérifiables produisent une efficacité et une précision supérieures.

L'article conclut que Hermes représente un mouvement vers des agents de raisonnement mathématique scalables, vérifiables et interprétables, comblant efficacement le fossé entre la flexibilité des LLM et la rigueur de la preuve de théorèmes formelle.