MolLean oblige les LLM à vérifier la chimie : un gain sur 12 tâches sur 12

Les raisonnements chimiques des modèles de langage paraissent souvent convaincants tout en contenant des affirmations inventées : le modèle décrit avec assurance une structure qui n'existe pas, ou attribue à une molécule des propriétés qu'elle n'a pas. Les auteurs de MolLean proposent de vérifier ces affirmations par programme. Ils ont créé un langage à vérification de processus, dans lequel chaque étape du raisonnement est rattachée à un état explicite de la molécule et passe par un noyau basé sur Lean. Sur 8 800 exemples appariés couvrant 12 tâches, avec le modèle Qwen3.6-27B, le mode d'affinage de la trace entière a devancé le chain-of-thought classique dans chacune des tâches.

La molécule comme état qu'on ne peut pas corrompre

Dans un chain-of-thought classique, le modèle rédige son raisonnement sous forme de texte, et personne ne vérifie s'il correspond à la molécule réelle. Avec MolLean, le raisonnement devient une trace exécutable. Il existe un état moléculaire courant, et chaque étape le modifie selon des règles strictes.

Le noyau est organisé en couches. En bas se trouvent les modifications primitives du graphe moléculaire ; au-dessus s'assemblent des transformations composées. Par-dessus, des affirmations portent sur les indicateurs moléculaires. Lorsque le modèle déclare qu'après une modification la molécule a gagné un groupe donné ou qu'un indicateur a changé, le noyau confronte l'affirmation à l'état au lieu de le croire sur parole.

Une règle importante a été adoptée : une action rejetée laisse l'état intact. Une étape erronée ne contamine donc pas la suite du raisonnement. Le modèle reçoit un refus et tente un autre coup à partir du même point.

Des témoins pour les mesures externes

Tout en chimie ne se déduit pas de la structure du graphe. Certaines propriétés proviennent de calculs ou de mesures externes. Pour ne pas mélanger ce qui est fiable et ce qui est admis sur la foi d'une source, les auteurs ont introduit un protocole de témoins typés. Il sépare les vérifications structurelles natives, que le noyau effectue lui-même, des données fournies de l'extérieur.

La trace indique ainsi quelles affirmations sont prouvées au sein du système et lesquelles reposent sur une source externe. Pour un audit, la différence est essentielle : un relecteur ou un chimiste voit immédiatement où la vérification est stricte et où la confiance est déléguée.

Trois modes et 8 800 exemples

MolLean propose trois modes d'utilisation :

• exécution unique de la trace : le modèle écrit tout le raisonnement, le noyau l'exécute ;
• affinage de la trace entière : après vérification, le modèle reçoit le résultat et réécrit l'ensemble du raisonnement ;
• mode interactif via MolLean-MCP : le modèle agit pas à pas et reçoit un retour directement pendant la génération.

MolLean-MCP est une interface d'outils à état (stateful). Elle expose au modèle les transitions entre états, les résultats des vérifications et les indicateurs moléculaires. C'est à partir de ces éléments que le modèle décide de la prochaine action.

La comparaison a été menée avec un chain-of-thought direct sur 8 800 exemples appariés. Ils couvrent 12 tâches : génération de molécules, édition, optimisation et réactions. Le modèle de base est Qwen3.6-27B.

Résultats clés :

• l'affinage de la trace entière fait mieux que le chain-of-thought direct dans les 12 tâches ;
• MolLean-MCP complète ce mode par un retour pas à pas ;
• sur les tâches de réactions, le mode interactif donne le meilleur résultat.

Ce dernier point est logique. Une réaction est une chaîne de transformations où une erreur précoce fait échouer tout le reste. Une vérification après chaque étape l'attrape immédiatement, plutôt qu'à l'analyse finale de toute la trace.

À quoi cela peut servir en pratique

Le modèle de 27 milliards de paramètres sert ici plutôt de démonstration : la couche de vérification ne dépend pas de la taille du modèle et peut accompagner d'autres LLM. Pour les équipes qui conçoivent des assistants en chimie médicinale ou en planification de synthèse, l'approche suggère une architecture concrète. Le modèle ne doit pas se contenter de produire du texte, mais appeler des outils qui conservent l'état et rejettent les étapes inadmissibles.

Le pattern lui-même est utile aux développeurs d'agents. L'état transactionnel avec annulation des actions rejetées, le noyau formel de vérification et la séparation entre contrôles propres et données externes se transposent à d'autres domaines où le raisonnement a un sens formel. On pense à la science des matériaux, à la biologie et à la conception de circuits.

Les limites sont également claires. Le gain a été mesuré sur un seul modèle et sur un ensemble donné de 12 tâches. La vérification des mesures externes continue de dépendre de la qualité de ces mesures. Mais le changement d'approche est net : les affirmations chimiques du modèle cessent d'être du texte libre et deviennent des engagements qu'on peut vérifier et réviser.