Incroyable, ce nomGaussLe nouvel agent IA de (Gauss) semble un peu fou. Parce qu'il utilise uniquementtrois semainesle temps, c'est faitTerence Taoet le défi mathématique d'Alex Kontorovich consistant à formaliser le théorème des nombres premiers (PNT) dans Lean.


Vous savez, après que Tao Zhexuan et Kontorovich ont proposé ce défi en janvier 2024, ils ont passé beaucoup de temps18 mois(juillet de cette année), des progrès progressifs n’ont été réalisés.

Alors quelle est l’origine de ce Gauss ?

Derrière c'est une entreprise appeléeMathématiquesSociété d'IA, selon les rapports, Gauss est la première à aider les meilleurs mathématiciens dans la vérification formelleformalisation automatique(autoformalisation)Agent :


La formalisation fait ici référence à la conversion d'un contenu mathématique écrit par des humains en un langage formel lisible par machine, vérifiable, strict et sans ambiguïté, puis à l'utilisation d'ordinateurs pour aider à vérifier son exactitude.

La raison pour laquelle Tao Zhexuan et Alex Kontorovich n’ont fait que des progrès progressifs jusqu’à présent est que le problème reste bloqué sur le problème central de l’analyse complexe.

En tant que vie à base de silicium, ce Gauss se caractérise par sa capacité à travailler sans arrêt, ce qui réduit considérablement la charge de travail que seuls les meilleurs experts formels pouvaient accomplir dans le passé ; dans le même temps, Gauss a également formalisé les principaux résultats manquants dans l'analyse complexe mentionnée ci-dessus.

C’est pourquoi il peut résoudre en trois semaines le défi mathématique que Terence Tao n’a pas réussi à relever en 18 mois.

Comment Gauss est-il implémenté ?

À l’heure actuelle, Math Company n’a pas officiellement publié de rapport technique spécifique.

Mais à en juger par le résultat final, Gauss a généré environ 25 000 lignes de code Lean, contenant des milliers de théorèmes et de définitions.

Vous savez, les preuves formelles de cette ampleur prenaient souvent de nombreuses années.

Les plus grands projets formels de l'histoire (s'étendant souvent même sur 10 ans) ne sont qu'un ordre de grandeur plus grand que cela (jusqu'à 500 000 lignes de code).

En comparaison, la bibliothèque mathématique standard de Lean, Mathlib, compte environ 2 millions de lignes de code et contient 350 000 théorèmes, mais il a fallu 8 ans à plus de 600 contributeurs pour la construire.


Afin de soutenir le fonctionnement de Gauss, l'équipe a également coopéré avec Morph Labs pour développer l'infrastructure environnementale Trinity.

Parce que faire fonctionner Gauss à si grande échelle impliquera des milliers d’agents simultanés, et chaque agent possède son propre environnement d’exploitation Lean, qui consommera plusieurs téraoctets de mémoire de cluster, ce qui en fera un défi d’ingénierie système extrêmement complexe.

L’équipe Math a également déclaré :

Gauss réduira considérablement le temps nécessaire pour réaliser de grands projets mathématiques.

À mesure que les algorithmes continuent de s’améliorer, nous prévoyons d’augmenter la quantité totale de code formel de 100 à 1 000 fois au cours des 12 prochains mois.

Ce sera le terrain de formation pour de nouveaux paradigmes – vers une « superintelligence vérifiable » et des « mathématiciens machines généralistes ».

Et tout à l'heure,Terence TaoJ'ai expliqué certains problèmes liés à la formalisation sur Mastodon (ce qui suit est la déclaration de Tao Zhexuan).

Les projets, quelle que soit leur complexité, ont tendance à avoir des objectifs explicitement déclarés et des objectifs implicites non déclarés. Par exemple, l’objectif déclaré d’un projet de formalisation Lean pourrait être d’obtenir une preuve formelle d’une proposition mathématique… ; apprendre à utiliser une variété d'outils collaboratifs et à attribuer des tâches ; découvrir organiquement la structure plus fine des preuves de

Dans le passé, il n’était souvent pas nécessaire d’articuler ces objectifs implicites car il existait une forte corrélation empirique entre la réalisation de ces objectifs et la réalisation d’objectifs explicites. Dans le cas des projets formels, presque tout effort centré sur l’humain pour atteindre des objectifs explicites permettra finalement et naturellement d’atteindre la plupart des objectifs implicites mentionnés ci-dessus. Ainsi, les objectifs explicites deviennent effectivement une alternative viable aux objectifs pratiques plus larges.

Cependant, les choses changent avec l’émergence d’outils d’IA puissants qui adoptent des approches très différentes de celles des humains. Ces outils peuvent être orientés pour résoudre un objectif explicite sans avoir à atteindre tous les objectifs implicites qui pourraient être atteints simultanément si la tâche était exécutée par une équipe humaine. En fait, la nature des algorithmes d’optimisation de l’IA fait qu’ils peuvent même atteindre des performances élevées sur des objectifs explicites au détriment de tous les objectifs implicites. (Voir la loi de Goodhart : « Lorsqu'une mesure devient un objectif, elle cesse d'être une bonne mesure. »)

Compte tenu du déploiement croissant de ces outils, cela me suggère que les organisateurs de projets doivent désormais faire un plus grand effort pour articuler clairement tous les objectifs d'un projet, et pas seulement les objectifs nominaux. Dans certains cas, ces objectifs peuvent même ne pas être évidents au départ pour les organisateurs eux-mêmes et peuvent nécessiter une discussion entre les participants. Les parties externes intéressées à tester de tels projets avec leurs outils d'IA doivent se coordonner à l'avance avec les organisateurs au cas où elles manqueraient un ou plusieurs objectifs implicites clés que leurs outils n'optimiseraient pas.


Le fondateur est l’auteur du ICML’25 Time Test Award

Il est à noter que le patron de la société Math a aussi une certaine force.

Parce qu’il est l’un des auteurs de l’article qui a remporté le prix ICML Time Test Award lors de la conférence sur l’IA de cette année.Christian Szegedy.


Cet article est la normalisation par lots (Batch Normalization, appelée BatchNorm) proposée par lui et un autre auteur Sergey Loffe en 2015.


Aujourd'hui, cet article a été cité plus de 60 000 fois. Il s’agit d’une avancée majeure dans l’histoire du développement de l’apprentissage profond et a grandement favorisé la formation et l’application de réseaux neuronaux profonds.

On peut dire qu’il s’agit de l’une des technologies clés qui permettent à l’apprentissage profond de passer d’expériences à petite échelle à une fonctionnalité et une fiabilité à grande échelle.

Bien sûr, même si les internautes se sont exclamés « Amazing » après avoir lu Gauss, ils ont également appelé le responsable à publier rapidement le journal.

Quant au contenu technique plus détaillé, nous pouvons y jeter un œil~