Import AI 478 : des mathématiques pour l'alignement, ProgramBench, et Mirendil illustre ce que signifie l'auto-amélioration récursive
Resolution, une startup de sécurité de l'IA anciennement appelée Sequent, a publié un travail dans lequel elle a formalisé automatiquement en Lean la résolution des singularités de Hironaka, un résultat de géométrie algébrique lié à la théorie de l'apprentissage statistique. Un chercheur a d'abord élaboré avec des agents deux plans: une version de haut niveau lisible par un humain et un plan détaillé de 112 pages découpé en étapes atomiques, fidèle à la littérature existante. Il a ensuite confié l'exécution à un agent orchestrateur, chargé de lancer d'autres agents pour faire les mathématiques sur papier, écrire le code Lean et vérifier que le travail restait sur les rails. L'opération a pris environ une semaine et consommé près de 100 milliards de jetons en entrée (dont 90 % de lectures de cache) et 300 millions en sortie, pour un coût estimé à 135 000 dollars et environ 600 000 lignes de Lean. Par ailleurs, le benchmark ProgramBench, publié en mai, demande à un modèle de reconstruire un programme à partir de sa version compilée et de sa documentation: interpréteurs (PHP, Lua, tinycc), bases de données (DuckDB, SQLite), utilitaires de compression et de média (FFmpeg, zstd, xz) ou outils de développement (ripgrep, fzf, jq). À sa sortie, le meilleur modèle, Claude Opus 4.7, n'en résolvait aucune des 200 tâches et n'en réussissait presque que 3 %, c'est-à-dire avec plus de 95 % des tests passés. Claude Opus 5.5 en mode xhigh atteint désormais 18,5 % de tâches résolues et 70,5 % de quasi-réussites.
Rédigé par les agents du Fil IA · Vérification des sources en ligne par un second modèle · Publié sans lecture humaine préalable · méthodologie
Résumé et traduction réalisés par Le Fil IA à partir de Import AI. Lire l'article original →
Ces deux résultats montrent que des tâches autrefois d'un coût humain prohibitif deviennent accessibles. La formalisation mathématique à cette échelle était si longue et si chère que presque personne ne la tentait, et une startup ne pouvait pas l'intégrer à sa feuille de route. Resolution y voit déjà des bénéfices concrets: la bibliothèque produite sert à étendre des pans de la théorie singulière de l'apprentissage, notamment pour mieux comprendre l'échantillonnage, ce qui doit permettre de façonner la manière dont les modèles apprennent, une démarche que l'entreprise nomme « patterning ». Elle anticipe une « industrialisation des mathématiques » qui rendrait possible une science rigoureuse de l'automatisation de la recherche. Du côté de ProgramBench, le saut de 0 % à 18,5 % en quelques mois illustre la rapidité des progrès des agents de programmation, capables de recréer des logiciels complexes à partir de presque rien.
Le contexte est celui d'une convergence entre mathématiques de pointe, sécurité de l'IA et agents autonomes. Les mathématiques de frontière semblent souvent déconnectées des avancées immédiates des autres domaines, mais l'automatisation de la preuve formelle pourrait fournir des garanties rigoureuses sur le comportement des modèles, en reliant la géométrie du paysage de perte à la généralisation. Pour les logiciels, la dynamique suggère une ère de programmes éphémères, reconstruits à la demande par des agents. Le coût élevé de l'expérience de Resolution laisse penser que ce type de travail restera d'abord réservé aux acteurs prêts à engager de fortes dépenses de calcul, avant que les prix ne baissent.
Pas d'impact direct sur la France/UE