David Silver quitte DeepMind, leve 1 milliard et parie contre les LLMs¶
Resume¶
David Silver, createur d'AlphaGo/AlphaZero et veterant de 15 ans chez DeepMind, lance Ineffable Intelligence a Londres. Levee de 1 milliard de dollars a 4 milliards de valorisation (Sequoia lead, interet Nvidia/Google/Microsoft). These centrale : les LLMs ne sont pas le chemin vers la superintelligence — il faut une nouvelle forme de reinforcement learning.
Sources : Fortune (30 jan 2026, exclu depart Silver), The Decoder (21 fev 2026, detail levee Sequoia), Sifted/FT (18 fev 2026, confirmation interet Nvidia/Google/Microsoft).
Analyse critique¶
La these de Silver¶
Les LLMs generent du texte plausible, mais ne decouvrent pas de connaissance nouvelle. Les "decouvertes IA" les plus citees viennent de systemes RL, pas de LLMs purs :
| Systeme | Domaine | Approche | Resultat |
|---|---|---|---|
| AlphaFold | Biologie structurale | RL + prediction | Structure de 200M proteines |
| AlphaProof | Mathematiques | RL + LLM (formulation) | 100M preuves generees |
| FunSearch | Algorithmique | RL + exploration | Nouvelles fonctions mathematiques |
| AlphaGo/Zero | Jeux | RL pur (self-play) | Surhumain sans donnees humaines |
Le pattern : le LLM formule (langage → structure), le RL explore (espace de solutions). Le LLM seul ne suffit pas pour la decouverte.
Le debat dans la conversation¶
@0xLalice challenge : "Bullshit. Les IA ont apporte du nouveau en biologie, algorithmique, maths."
@iamsupersocks precise : "T'as raison de challenger, mais la nuance est importante. La plupart des decouvertes qu'on cite viennent de systemes RL, pas du LLM pur." — C'est la distinction cle. Les LLMs sont le front-end (formuler, traduire), le RL est le moteur de decouverte.
@kaizenbuild sur le timing : "Le point le plus interessant, c'est presque moins le montant que le timing. Quand quelqu'un comme Silver part maintenant, ca veut dire qu'il pense que la fenetre est ouverte pour une autre trajectoire."
@iamsupersocks confirme : "Exactement pareil pour LeCun — ou bien trop de conflit en interne avec leur vision." — Silver n'est pas le seul. LeCun (Meta) pousse aussi une vision post-LLM (world models). Deux poids lourds du meme cote.
@Nunenthal contreargumente : "C'est masque le fait que les LLMs s'entrainent desormais sur des donnees synthetiques pour depasser cette limite fondamentale. Et les world models se heurtent au manque de donnees d'entrainement." — Point valide : les donnees synthetiques + RL (comme o1/o3 d'OpenAI) brouillent la frontiere LLM vs RL.
@seo_mintavocado rappelle : "Google/DeepMind le dit depuis le debut — les IA actuelles sont des etapes vers un but plus grand." — L'interne DeepMind a toujours vu les LLMs comme transitoires.
Ce qui est solide¶
- Le pedigree est incontestable. Silver n'est pas un commentateur — c'est l'auteur d'AlphaGo, AlphaZero, et co-auteur de l'article fondateur du deep RL. Quand il dit que les LLMs ne suffisent pas, ca a du poids.
- 1 milliard leve a Londres, pas dans la Silicon Valley. Signal fort pour l'ecosysteme IA europeen.
- Le timing : Silver part au moment ou DeepMind est absorbe dans Google et ou la recherche fondamentale y perd du terrain face au produit (Gemini). Il rejoint LeCun dans le camp "post-LLM".
Ce qui est a nuancer¶
- "Contre les LLMs" est une simplification mediatique. En pratique, les meilleurs systemes combinent LLM + RL (AlphaProof utilise un LLM pour formuler les preuves, RL pour les explorer). Silver ne dit pas "les LLMs sont inutiles", il dit "les LLMs seuls ne suffisent pas pour la superintelligence".
- 1 milliard pour du RL fondamental sans produit visible — c'est un pari a horizon 5-10 ans.
- La frontiere LLM/RL se brouille : o1, o3 (OpenAI) et les modeles "reasoning" sont des LLMs entraines avec du RL. Le debat n'est peut-etre pas LLM vs RL mais "scaling de l'existant" vs "rupture architecturale".
Le vrai clivage¶
| Camp | Champion | These | Approche |
|---|---|---|---|
| Scaling | OpenAI, Anthropic | Plus de compute + donnees synthetiques = AGI | LLM + RL pour raisonner |
| Rupture RL | Silver (Ineffable) | RL fondamentalement nouveau | Au-dela des LLMs |
| World models | LeCun (Meta/FAIR) | Modeles du monde, pas juste du langage | Post-LLM, non RL pur |
| Hybride | DeepMind (interne) | LLMs = etape, pas destination | Combinaison progressive |
Trois visions post-LLM (Silver, LeCun, DeepMind interne) contre une vision scaling (OpenAI/Anthropic). Le marche tranchera.
Pertinence ProbatioVault¶
Impact faible et indirect a court terme, mais structurant a long terme.
Le workflow de gouvernance ProbatioVault est construit sur les LLMs (Claude, ChatGPT, Llama). Si Silver a raison et que les LLMs plafonnent, ca ne change rien immediatement — les LLMs actuels sont deja suffisants pour specifier, implementer et reviewer du code.
Ce qui est pertinent : - Agnosticisme modele : le workflow est declaratif (assignees Jira). Si demain un modele RL-based est meilleur pour les reviews de securite, on change l'assignee. Zero code modifie. C'est exactement le bon positionnement face a cette incertitude. - Les "grands noms" divergent : Silver, LeCun, DeepMind interne — trois visions differentes du post-LLM. Ca renforce la decision de ne pas s'enfermer dans un provider unique. - Le pattern LLM formule + RL explore est exactement ce que fait le workflow : le LLM genere (spec, code), la gate deterministe juge (scoring mathematique, pas LLM-as-Judge). Le jugement n'est pas delegue au LLM. Silver approuverait.
Interet pour la verification formelle ProbatioVault¶
Le pipeline ProbatioVault-formal suit deja le pattern AlphaProof : 1. extract-facts.py extrait des faits depuis le code (AST + normes) → le LLM formule 2. TLC/Alloy/Prolog verifient les proprietes → le solveur juge
Le risque identifie (et documente dans le tweet a @JuWeb1) est la circularite : si les faits extraits re-decrivent le code au lieu de le confronter aux exigences normatives, la preuve est tautologique. Le solveur dit "vrai" parce que le modele dit la meme chose que le code.
AlphaProof resout le probleme inverse (explorer des preuves pour un enonce bien pose). Chez ProbatioVault, c'est la formulation des enonces qui est le point faible, pas la recherche de preuve.
Ce qui est actionnable sans AlphaProof : ajouter une phase generation adversariale de contre-exemples dans le pipeline formal. Principe : 1. Demander a un LLM de proposer des scenarios ou le code DEVRAIT echouer (etats limites, violations de normes, cas degeneres) 2. Verifier que le modele formel detecte bien ces violations 3. Si le modele ne les detecte pas → les proprietes sont trop faibles (= tautologies deguisees)
C'est du model checking adversarial — proche de l'AlphaZero self-play (jouer contre soi-meme pour trouver les failles). Et c'est faisable avec Claude/ChatGPT aujourd'hui, sans infrastructure RL.