Anthropic PBC a utilisé Claude pour créer une version vérifiable par ordinateur d'une preuve mathématique célèbre et très compliquée.
L'entreprise a détaillé le projet dans un article de blog publié aujourd'hui.
Une preuve est une série d’arguments qui prouvent qu’une hypothèse mathématique est correcte. La preuve abordée par Anthropic vérifie une hypothèse appelée le dernier théorème de Fermat. Initialement lancée en 1637, l'hypothèse se concentre sur les propriétés des nombres entiers positifs.
La preuve du dernier théorème de Fermat a été développée en 1995 par le mathématicien Andrew Wiles. Il compte 129 pages et sa vérification a nécessité des mois de travail. Le projet de recherche d'Anthropic a formalisé la preuve de Wiles, ce qui signifie que l'entreprise l'a transformée en une forme pouvant être automatiquement vérifiée par des ordinateurs. La formalisation des preuves est utile car elle exclut la possibilité d’erreur humaine et facilite le partage d’informations entre mathématiciens.
Une preuve formalisée prend la forme d’un extrait de code écrit dans un langage de programmation appelé Lean. C'est une syntaxe spécialisée que les mathématiciens utilisent pour vérifier des hypothèses. La preuve d'Anthropic comprend 13 millions de lignes de code Lean, ce qui en fait le plus gros fichier de ce type jamais créé.
La formalisation est difficile car les preuves ont tendance à être assez laconiques. Il leur manque certaines explications dont un ordinateur aurait besoin pour les comprendre, ce qui oblige les développeurs Lean à ajouter les explications manuellement. Une autre source de complexité réside dans le fait que les arguments d’une preuve s’appuient souvent les uns sur les autres. Cela signifie qu’une ligne erronée de code Lean peut rendre invalide tout le code suivant.
Les mathématiciens s'attendaient à ce que le processus de formalisation de la preuve de Wiles prenne plusieurs années. Selon Anthropic, ses chercheurs ont réalisé la tâche en 11 jours en utilisant un modèle de recherche interne. L'algorithme est décrit comme étant à peu près comparable à Claude Fable 5.1, le prédécesseur immédiat de GPT-6 Astra.
Notamment, le modèle a accompli la tâche en utilisant seulement une quantité limitée d’apports humains de haut niveau. Il a fait tourner plusieurs dizaines d'agents qui ont généré 6 milliards de jetons de sortie tout en travaillant sur la preuve. Chemin faisant, ils ont prouvé pas moins de 29 500 théorèmes intermédiaires.
La tentative initiale d'Anthropic pour formaliser la preuve de Wiles a échoué. Selon l'entreprise, la percée a eu lieu lorsqu'elle a donné à Claude l'accès à un outil open source appelé Prove2Me. Le logiciel permet aux agents IA de déterminer plus facilement la prochaine étape optimale dans un long flux de travail de traitement. Prove2Me permet également de réduire les coûts d'inférence.
« Nous assistons à l'autoformalisation de l'algèbre, de l'analyse harmonique, de la géométrie et de la théorie des nombres, et nous apprenons que les artefacts d'autoformalisation de l'IA sont désormais suffisamment robustes pour être construits ; la preuve est à plusieurs niveaux », a déclaré Kevin Buzzard, un mathématicien dont Claude a utilisé le travail pour générer sa preuve formalisée.
Cette étape importante intervient un mois après Anthropic détaillé une autre avancée mathématique basée sur le LLM. L'entreprise a utilisé Claude pour découvrir de nouvelles informations sur la fonction zêta de Riemann, un objet mathématique étroitement étudié. C’est le point central de l’hypothèse de Riemann, l’une des conjectures les plus difficiles au monde.
Rival OpenAI Group PBC exploite également ses LLM pour faire progresser la recherche en mathématiques. Le mois dernier, l'entreprise a utilisé son dernier modèle Astra pour résoudre plusieurs problèmes d'Erdos et affiner un certain nombre de questions ouvertes en informatique théorique.
