Faire communiquer un modèle de langage et un assistant de preuve

Les grands modèles de langage (LLMs pour Large Language Models) sont des modèles d’intelligence artificielle capables de générer du texte en langage naturel. Entraînés sur d’immenses quantités de données, ces modèles sont au cœur d’applications comme ChatGPT (openAI) ou Le Chat (Mistral). Grâce à des développements récents, ces modèles sont de plus en plus utilisés pour des tâches allant de la génération de code à la résolution de problèmes mathématiques à partir de descriptions en langage naturel. Mais que veut dire raisonner pour ces modèles ? Peut-on se fier aux résultats ?

D’un autre côté, les assistants de preuve tels que Rocq permettent de valider une preuve mathématique avec un très haut niveau de confiance, mais l’expertise nécessaire pour utiliser ces outils les rend difficiles d’accès.

Faire communiquer efficacement un LLM et un assistant de preuve permettrait d’atteindre deux objectifs complémentaires. D’abord, l’assistant de preuve peut valider les raisonnements générés par un LLM. Ensuite, les LLMs offrent une interface conversationnelle intuitive qui peut faciliter l’utilisation de ces assistants jusque-là réservés aux experts.

Deux lois d’échelle pour les LLMs

On assiste aujourd’hui à une course mondiale pour développer des modèles de plus en plus puissants. Les chiffres donnent le tournis : les modèles les plus récents contiennent des centaines de milliards de paramètres, sont entraînés sur des milliards de textes d’origines diverses, et leur coût d’entraînement est estimé à des dizaines de millions de dollars. Pour donner un exemple récent, le modèle DeepSeek-V3 contient 671 milliards de paramètres et son entraînement a demandé près de 3 millions d’heures GPU (les processeurs graphiques utilisés pour les calculs intensifs). Si ce modèle a fait les gros titres parce que son entraînement a été incroyablement efficace pour sa taille, il aura quand même coûté environ 6 millions de dollars.

La course aux grands modèles s’explique par une observation simple : les performances augmentent avec la taille des modèles. Plus précisément, lors de l’entraînement, les paramètres (des milliards de nombres qui contrôlent le comportement du modèle) sont ajustés pour optimiser un objectif qu’on appelle la perte. Dans le cas des modèles de langage comme les LLMs, on demande au modèle de compléter un texte connu (partiellement masqué) et la perte mesure la distance entre le texte généré et le texte original. Par exemple, « Le petit chat est mort. » est très proche de « Le petit chat est fort. » mais assez loin de « Le ciel est bleu aujourd’hui. ».

Or, on a observé dès 2020 une loi d’échelle pour l’entraînement des LLMs : la perte évolue selon une loi de puissance avec la quantité de calcul (nombre de paramètres, tailles de corpus d’entraînement, et temps d’entraînement). Et plus la perte est faible, plus les modèles deviennent performants pour diverses tâches : résumer, extraire de l’information, faire des raisonnements mathématiques, générer du code informatique, etc. Il est par ailleurs possible de spécialiser les LLMs sur une tâche spécifique en complétant leur entraînement sur des données ciblées.

Beaucoup plus récemment, on a également observé une nouvelle loi d’échelle pour l’inférence : les performances d’un modèle augmentent aussi avec la taille du texte généré lors de son utilisation. Confronté à une question, les modèles récents commencent par générer un long texte appelé chaîne de pensées qui imite un comportement humain. En utilisant le contenu de la chaîne, le modèle peut ensuite synthétiser un résumé.

Voici par exemple un exercice issu d’un jeu de données d’exercices de lycée utilisé pour évaluer les LLMs (traduit en français ici).

Des tubes de peinture contiennent 8 centilitres d’un mélange de jaune et de bleu. Il y a du bleu et du jaune dans chaque tube. Mon premier tube contient un quart de la quantité totale de jaune et un sixième de la quantité totale de bleu. Combien y a-t-il de tubes ?

Si certaines applications (comme ChatGPT) masquent les chaînes de pensées, on peut parfois demander au modèle de nous montrer tout le texte généré. Voici par exemple la chaîne de pensées générée par DeepSeek-R1 pour ce problème (attention spoiler, le raisonnement original en anglais a été traduit).

On peut voir le modèle essayer plusieurs approches, se corriger, vérifier ses résultats, presque comme un étudiant en train de passer un examen devant un tableau noir. Le texte est ponctué d’expressions comme : « Ok, essayons de déterminer », « peut-être pouvons-nous supposer », « Attendez », « Hmm », « Est-ce possible », « laissez-moi vérifier » qui incitent le modèle à continuer la génération de texte pour progresser dans le raisonnement. Le modèle peut ensuite synthétiser une réponse courte et structurée en résumant cette chaîne de pensées. Les LLMs les plus récents, dits modèles de raisonnement, sont spécialisés lors de l’entraînement pour générer ces chaînes de pensées.

Cette nouvelle loi d’échelle ne s’arrête pas aux chaînes de pensées. Plutôt que d’investir toute la puissance de calcul au moment de l’entraînement, on utilise maintenant les ressources de calcul pour exploiter au mieux les textes générés. Une technique simple consiste à générer plusieurs chaînes de pensées en parallèle avant de choisir celles qui ont donné les meilleurs résultats. On peut également utiliser des algorithmes de recherche arborescente : à chaque étape de raisonnement, on génère plusieurs solutions, mais on ne fait progresser que les plus prometteuses.

En combinant toutes ces approches, il est aujourd’hui possible de spécialiser de relativement petits modèles qui atteignent des performances comparables à celles des énormes LLMs les plus connus (GPT-4o, Claude Sonnet, Gemini) pour un budget beaucoup plus modeste.

Ces nouveaux développements posent une question fondamentale : comment vérifier les raisonnements produits par les LLMs ? Cette question, qui était déjà préoccupante pour les premiers LLMs, devient cruciale pour les modèles de raisonnement pour lesquels une hallucination (une information fausse et inventée) peut complètement fausser la chaîne de pensées.

On construit donc des agents : des applications capables de coupler les LLMs avec des outils externes pour valider le texte généré (par exemple pour faire des recherches sur le web, ou pour exécuter du code généré par le LLM), et des algorithmes de recherche.

Valider les chaînes de pensées avec un assistant de preuve

Fruit d’un travail à l’intersection de la logique mathématique et la théorie des langages de programmation, les assistants de preuve sont des outils qui permettent à un ordinateur de vérifier un raisonnement mathématique. Une preuve est décomposée en étapes logiques et l’ordinateur vérifie que chaque étape respecte les règles de la logique mathématique. Si une preuve repose sur l’utilisation d’un théorème, l’ordinateur vérifie que toutes les hypothèses sont bien vérifiées et que la conclusion suffit à prouver le résultat attendu

Les assistants de preuve comme Rocq (anciennement Coq), Lean ou Isabelle sont des outils interactifs. L’utilisateur propose une étape de raisonnement que l’ordinateur vérifie avant d’indiquer à l’utilisateur ce qu’il reste à démontrer. Prenons un exemple très classique :

Tous les hommes sont mortels. Socrate est un homme. Donc, Socrate est mortel.

Le but initial est de prouver Socrate est mortel. Pour prouver ce théorème, on peut commencer par spécialiser la première prémisse Tous les hommes sont mortels à l’individu Socrate. L’assistant ajoute alors une nouvelle hypothèse : Si Socrate est un homme alors Socrate est mortel. On applique alors la seconde prémisse Socrate est un homme à cette hypothèse et l’assistant vérifie qu’on obtient bien Socrate est mortel.

En théorie, ce fonctionnement interactif est parfaitement adapté pour développer un agent capable de vérifier un raisonnement mathématique. Chaque étape de raisonnement est validée par l’assistant de preuve, et les réponses (ou les messages d’erreur) de l’assistant de preuve nourrissent le LLM pour générer les prochaines étapes de raisonnement. Malheureusement, cet exercice de formalisation reste particulièrement difficile pour les humains comme pour les LLMs. Des LLMs récents sont aujourd’hui très performants pour la génération de code, mais l’exercice de preuve formelle ajoute une contrainte fondamentale qui rend l’exercice beaucoup plus compliqué : la preuve n’est terminée que si le code est parfaitement correct. Il n’y a aucune approximation possible. Par ailleurs, le code doit être écrit dans un langage spécialisé dont il existe relativement peu d’exemples au milieu des immenses quantités de données utilisées lors de l’entraînement.

Pour utiliser au mieux les capacités des LLMs, on peut réutiliser l’idée des chaînes de pensées. Plutôt que d’essayer de générer directement du code, on demande au modèle de décrire le théorème et ses hypothèses en langage naturel (par exemple en anglais ou français) et de suggérer un schéma de preuve, avant de générer le code en résumant la chaîne de pensées.

Couplé avec des algorithmes de recherche, cette approche commence à donner des résultats impressionnants sur des exercices de niveau lycée ou licence [1-2-3]. En utilisant une technique d’apprentissage « par renforcement » AlphaProof, un modèle entraîné par Google Deepmind sur des millions de théorèmes générés automatiquement, a même réussi à prouver avec l’assistant de preuve Lean des problèmes d’olympiades de mathématiques, atteignant le niveau d’une médaille d’argent.

Un assistant d’assistant de preuve

Les assistants de preuve sont donc des outils précieux pour valider les raisonnements générés par les LLMs. En changeant de perspectives, les LLMs peuvent également modifier en profondeur la manière dont nous utilisons des assistants de preuves qui restent aujourd’hui des outils réservés aux experts.

Si le code final doit être écrit dans un langage de programmation spécialisé, les chaînes de pensées générées lors du raisonnement sont écrites en langage naturel. Un humain peut donc facilement inspecter le raisonnement pour comprendre le code suggéré par l’assistant, voire directement intervenir pour le corriger. Les LLMs permettent ainsi de développer des interfaces conversationnelles :  il devient de plus en plus possible de « discuter » (en français ou en anglais) avec l’assistant de preuve pour formaliser un théorème sans être un expert du langage de programmation spécialisé.

Les logiciels d’édition de code intègrent déjà ce genre de technologies pour les langages les plus populaires comme Python ou JavaScript. Ces assistants rendent de nombreux services qui vont de l’autocomplétion (compléter un bout de code à partir du contexte et des commentaires) à l’analyse de documentation (par exemple pour retrouver une fonction ou un théorème à partir d’une description floue en langage naturel).

L’utilisation des LLMs pour les assistants de preuve est un domaine de recherche aujourd’hui très actif. On cherche à développer des agents capables de faciliter de nombreuses tâches qui restent difficiles ou ingrates pour les humains. Par exemple, en utilisant les impressionnantes capacités de traduction des LLMs, on aimerait traduire directement un livre de mathématiques (théorèmes et preuves) dans le langage de l’assistant de preuve. Cette tâche suppose d’être capable de comprendre le contexte, les hypothèses implicites propres à chaque domaine, et la nature des objets mathématiques manipulés. Les LLMs récents entraînés sur de très nombreux textes mathématiques (avec différents niveaux de rigueur) peuvent faire des associations d’idées pour combler les « trous » entre le langage naturel du livre et sa formalisation dans un assistant de preuve. Ce problème reste très difficile, mais une solution partielle générée par un LLM peut être un point de départ précieux pour un humain.

Enfin, le comportement d’un programme peut aussi être formalisé dans un assistant de preuve. Il est donc possible de prouver qu’un programme est correct. Par exemple, on peut prouver qu’une fonction de tri en Python ou JavaScript renvoie toujours un tableau trié. À plus long terme, on aimerait avoir des assistants capables de traduire une spécification en langage naturel vers un code exécutable, une formalisation de la spécification, et une preuve de correction qui montre que le code correspond bien à sa spécification. Les assistants de preuve aidés par des LLMs permettraient ainsi de garantir que le code généré par un LLM est bien correct ! C’est un enjeu crucial dans un monde où le code informatique des applications que nous utilisons tous les jours devient de plus en plus généré automatiquement par ces modèles.

Conclusion

Faire communiquer LLMs et assistants de preuve ouvre des perspectives prometteuses pour l’avenir de l’intelligence artificielle et de la vérification formelle. En combinant la capacité des LLMs à générer des raisonnements complexes en langage naturel avec la rigueur des assistants de preuve, il devient possible de développer des agents capables de vérifier des preuves mathématiques. Ces agents pourraient non seulement améliorer la fiabilité des résultats produits par les LLMs et les capacités de raisonnement des futures générations de modèles, mais aussi rendre les outils de preuve formelle aujourd’hui réservés à des experts plus accessibles.

Guillaume Baudart, Inria

• [1] https://arxiv.org/abs/2310.04353
• [2] https://hal.science/hal-04886208v1 
• [3] https://arxiv.org/abs/2408.08152

Note : Merci à Vincent Baudart, Paul-André Melliès, Marc Lelarge, Théo Stoskopf, Jules Viennot, et Sarah Winter pour leurs relectures et leurs suggestions.