Google DeepMind ouvre le code d'AlphaProof et fait entrer la vérification formelle des mathématiques dans l'ère des LLM
Le système qui a résolu des problèmes des Olympiades internationales de mathématiques en 2024 voit son code source et ses poids libérés, permettant aux chercheurs de coupler des modèles de langage à des prouveurs formels comme Lean
Google DeepMind a libéré le code source et les poids d'AlphaProof, le système qui a résolu en 2024 des problèmes des Olympiades internationales de mathématiques (IMO) en couplant un modèle de langage à un prouveur formel. Cette ouverture met entre les mains de la communauté de recherche l'une des architectures les plus influentes pour le raisonnement automatisé vérifiable.
La décision transforme ce qui était une expérience de laboratoire fermée en infrastructure ouverte pour les universités, les startups et les groupes indépendants qui travaillent sur des démonstrations mathématiques assistées par machine.
Comment le système fonctionne en pratique
AlphaProof ne génère pas de texte libre : il produit des preuves écrites dans le langage formel Lean, où chaque étape logique est vérifiée par un noyau indépendant. Si une étape ne tient pas, la preuve est rejetée — ce qui élimine une grande partie des hallucinations typiques des modèles de langage.
L'architecture combine un modèle de langage qui propose des stratégies de démonstration avec un mécanisme de recherche qui teste et affine chaque tentative contre le vérificateur. L'apprentissage se fait par renforcement, le système accumulant des preuves valides au cours de l'entraînement.
Pourquoi la vérification formelle compte
La vérification par Lean est devenue l'un des domaines les plus disputés de la recherche en IA. Contrairement à un chatbot qui répond avec assurance à une équation erronée, un système qui écrit des preuves formelles doit convaincre un vérificateur mathématique — pas un lecteur humain.
Cette propriété attire l'intérêt des laboratoires qui cherchent des modèles fiables pour l'ingénierie logicielle, la cryptographie et la découverte scientifique, des domaines où une erreur silencieuse coûte cher.
Ce qui change avec l'open source
Avec l'accès au code et aux poids, les chercheurs peuvent reproduire le pipeline d'entraînement, adapter le système à d'autres prouveurs formels et mesurer ses performances sur leurs propres benchmarks. L'ouverture permet aussi d'auditer les choix de conception de DeepMind.
Le mouvement suit la stratégie du laboratoire de publier des artefacts de recherche en mathématiques formelles, un domaine où la vérification par machine est devenue un standard de qualité scientifique.