Tu suis la course aux modèles IA ?
Chaque sortie (GPT, Claude, Gemini, Mistral…) décryptée le soir même, en 5 min. Gratuit.
Inclus dès l'inscription : notre sélection des meilleurs guides & comparatifs IA.
Choisis ton rythme
Gratuit · Pas de spam · Désabonnement en 1 clic
Des chercheurs de Cambridge et du King's College signalent des divergences entre des démonstrations en langage naturel et leurs versions en Lean dans des solutions publiées par OpenAI. Le groupe consultatif AGMAI relève des exigences non remplies, dont l'absence de métadonnées et l'usage de modèles propriétaires. Seules 10 publications sur 719 dévoilent la chaîne de pensée, et 42 % des preuves n'ont pas été formalisées.
Des divergences relevées entre texte et code Lean
Des mathématiciens de l'Université de Cambridge et du King's College de Londres ont identifié au moins deux divergences entre une preuve rédigée en langage naturel et son encodage en Lean pour une solution d'OpenAI à un problème dérivé des équations de Navier-Stokes. Le processus suivi par les modèles consiste à produire d'abord une explication en langage naturel, puis à tenter de la formaliser en Lean, un langage qui permet en principe de certifier la validité d'une preuve par compilation. Ces divergences ne remettent pas nécessairement en cause les solutions, mais elles soulèvent des doutes sur la fiabilité d'une auto-formalisation sans intervention humaine. Ils estiment que les preuves en langage naturel produites par OpenAI et d'autres preuves auto-formalisées en Lean ne devraient pas être considérées comme fiables sans un examen par les pairs et une rigueur équivalente à celle appliquée aux preuves traditionnelles.
Compréhension humaine et responsabilité encore incertaines
Melanie Wood, professeure à Harvard, souligne qu'une solution générée par un modèle ne bénéficie d'aucune compréhension humaine au moment de sa publication, et que le travail d'interprétation reste à accomplir par la suite. Terence Tao critique une approche où des utilisateurs d'IA résolvent des problèmes sans engagement envers le domaine, ni capacité à expliquer, enseigner ou dialoguer sur les résultats. Des mathématiciens rappellent que, dans la recherche traditionnelle, les auteurs assument la responsabilité de leurs découvertes et les diffusent par articles, conférences et séminaires, ce qui favorise la compréhension et l'application des solutions. Il n'est pas établi qu'OpenAI prenne la responsabilité de garantir cette compréhension humaine lors de la publication de ses preuves, comme le prévoient les principes de l'AGMAI.
Plusieurs écarts avec les recommandations de l'AGMAI
L'AGMAI a demandé d'inclure des métadonnées lisibles par machine reliant le langage naturel et les artefacts formels, ce qu'OpenAI n'a pas fait dans ses publications récentes. La première recommandation de l'AGMAI était également de ne pas tester de problèmes mathématiques avancés sur des modèles propriétaires, alors qu'OpenAI indique explicitement utiliser ses modèles propriétaires sur des problèmes de recherche ouverts. Sur le plan de la transparence, seules 10 publications sur 719 contiennent une chaîne de pensée du modèle, et 42 % des preuves publiées n'ont pas été formalisées. L'AGMAI précise qu'il revient à la communauté mathématique d'évaluer la mise en œuvre de ses recommandations et suggère qu'OpenAI contribue au financement du travail des mathématiciens nécessaires pour interpréter ces solutions.
Ce qu’OpenAI a livré et ce qui reste en débat
OpenAI a publié 719 manuscrits revendiquant des solutions à des problèmes mathématiques difficiles, en diffusant rapidement ses résultats et en fournissant des informations sur la méthode employée par ses modèles. Le laboratoire affirme avoir consulté un groupe consultatif de mathématiciens, l'AGMAI, hébergé par l'Institute for Advanced Study de Princeton et composé de neuf chercheurs. Ce groupe a publié des lignes directrices à la fin de septembre, mais n'a pas donné d'évaluation approfondie de cette vague de preuves. Des écarts existent entre la formulation en langage naturel et la formalisation pour un problème présenté comme valant un million de dollars. Des mathématiciens estiment qu'OpenAI n'a pas atteint les standards nécessaires, notamment en ce qui concerne la compréhension humaine des résultats.
