Aller au contenu principal

Un article tagués avec « Gemini Deep Think »

Voir tous les tags

Stanford CS329A (Ep 14): AlphaProof & Mathematical Reasoning — Vérification formelle, Lean 4, AlphaGeometry et Gemini Deep Think

· 10 minutes de lecture
Jaybee
AI & Robotics Engineer

Lors de notre cours précédent consacré au raisonnement des LLM, nous avons exploré comment le prompting par Chaîne de Pensée (Chain-of-Thought, CoT) et le décodage par Auto-Cohérence (Self-Consistency) ont initié le raisonnement causal multi-étapes au sein des réseaux neuronaux. Cependant, dans les domaines hautement critiques — tels que la vérification de protocoles cryptographiques, les logiciels de trajectoire orbitale ou les démonstrations de théorèmes mathématiques de pointe — le texte en langage naturel présente une faille intrinsèque :

"Quelle que soit l'éloquence et la clarté d'une chaîne de pensée en langage naturel générée par un LLM, elle demeure une séquence stochastique de tokens probabilistes. Une unique erreur subtile de signe, un raisonnement circulaire ou un lemme hallucinatoire anéantit l'ensemble de l'édifice. En mathématiques pures, une preuve correcte à 99% équivaut à une preuve correcte à 0%."

Bienvenue dans le Cours 14 de Stanford CS329A: Self-Improving AI Agents, second volet de la Partie 4 : Frontières (Frontiers in Reasoning & Autonomy). En nous appuyant sur les percées majeures dirigées par le Dr Thang Luong (Directeur de recherche senior chez Google DeepMind), nous étudions comment l'intelligence artificielle est passée de la prédiction statistique de mots à une déduction mathématique infaillible et vérifiée par machine, culminant par l'obtention de médailles historiques aux Olympiades Internationales de Mathématiques (OIM / IMO) :

  • AlphaGeometry (Nature 2024) : La synthèse neuro-symbolique unissant moteurs déductifs déterministes et Transformers génératifs pour les constructions géométriques auxiliaires.
  • AlphaProof (DeepMind, Nature 2025) : La transformation de la démonstration formelle de théorèmes en un jeu de plateau style AlphaZero grâce à Lean 4, à l'auto-formalisation et à l'apprentissage par renforcement au moment du test (TTRL).
  • Gemini Deep Think (IMO 2025) : Le triomphe du raisonnement pur en langage naturel et de la pensée parallèle (Parallel Thinking), décrochant la première médaille d'or officielle aux OIM (35/42) dans la limite humaine de 4,5 heures.
  • Vérification formelle et raisonnement mathématique par LLM : Comparaison approfondie entre noyaux formels typés par compilateur et apprentissage par renforcement non contraint.