Publication de preuves informatisées et réaction de la communauté scientifique
Pour générer ces démonstrations inédites, l'entreprise américaine a sollicité son modèle le plus évolué pendant une durée équivalente à trois heures de calcul par théorème. L'ensemble des résultats a été partagé sous le langage Lean, une solution logicielle créée pour valider des raisonnements logiques par ordinateur. Par cette démarche, la firme entend prouver que ses outils dépassent la prédiction de mots pour élaborer une logique complexe. Les directeurs des systèmes d'information pourraient y trouver des applications pratiques pour l'optimisation des architectures réseau ou des algorithmes financiers.
Toutefois, la méthode suscite une opposition majeure au sein de la recherche internationale. L'Association pour les mathématiques humaines qualifie cette initiative de « coup de communication », soulignant qu'elle intervient simultanément à des actions en justice relatives à la violation de droits d'auteur. Face à l'impossibilité d'expliquer le cheminement de l'intelligence artificielle, neuf chercheurs mondiaux de premier plan ont constitué un organe de contrôle totalement autonome. En France, l'École normale supérieure apporte son soutien à ce nouveau groupe consultatif, dont la tâche consiste à imposer des exigences de publication et d'audit aux grandes entreprises de la technologie.
En parallèle, la société OpenAI a concrétisé le rachat d'Orchestra Bio, une plateforme dédiée à la coordination du développement de médicaments entre intervenants humains et agents artificiels.
| Élément / Indicateur | Donnée de la source |
|---|---|
| Fichiers de démonstrations déposés sur GitHub | Plus de 700 |
| Temps de calcul par théorème | Environ 3 heures |
| Objectif de théorèmes à résoudre | Environ 100 |
| Langage de vérification utilisé | Lean |
| Nombre de chercheurs fondateurs de l'organe de contrôle | 9 |
À retenir
* OpenAI a publié plus de sept cents fichiers de démonstrations mathématiques sur la plateforme GitHub et vise la résolution de cent théorèmes. * Le processus a requis environ trois heures de calcul par théorème avec le modèle le plus avancé de l'entreprise, en utilisant le langage Lean. * Un collectif indépendant de neuf chercheurs internationaux, soutenu par l'École normale supérieure, exige des normes d'audit et de publication pour les géants technologiques. * L'Association pour les mathématiques humaines dénonce une opération de communication menée en pleine procédure judiciaire pour violation de droits d'auteur. * La firme américaine a également racheté la plateforme Orchestra Bio afin d'automatiser la préparation de traitements pharmaceutiques.
Sources
- Source : ZDNet France