OpenAI a publié cette semaine des centaines de solutions présumées à des problèmes mathématiques difficiles, dans le but de démontrer la capacité de ses modèles à traiter des problèmes avancés. Cependant, la publication n’a pas entièrement respecté les lignes directrices établies par un groupe consultatif de chercheurs en mathématiques, relançant la question fondamentale : suffit-il que les modèles produisent une solution susceptible d’être formalisée par un logiciel, ou celle-ci doit-elle aussi être compréhensible et vérifiable par les mathématiciens ?
Le groupe Advisory Group on Mathematics and Artificial Intelligence (AGMAI) compte neuf chercheurs éminents et est hébergé par l’Institute for Advanced Study de l’université de Princeton. Le groupe avait publié fin septembre des lignes directrices à l’intention des laboratoires qui développent des modèles avancés pour résoudre des problèmes mathématiques.
Un respect partiel des lignes directrices des chercheurs
AGMAI a indiqué que l’évaluation du respect de ses recommandations revenait en définitive à la communauté mathématique. L’une de ses principales recommandations est de cesser de tester les problèmes mathématiques avancés sur des modèles détenus par des entreprises commerciales, tandis qu’OpenAI a explicitement indiqué qu’elle utilisait des problèmes de recherche ouverts pour évaluer ses propres modèles.
OpenAI a suivi certains principes, comme la publication rapide des résultats et la fourniture d’informations sur la manière dont les modèles sont parvenus à leurs conclusions. Toutefois, seuls 10 manuscrits sur 719 incluaient les chaînes de raisonnement du modèle. En outre, 42 % des preuves publiées n’ont pas fait l’objet d’une formalisation.
Le groupe estime que les preuves difficiles à comprendre pour les humains devraient être converties dans un format formel. Il a toutefois également souligné la responsabilité du laboratoire de veiller à ce que la publication des résultats s’accompagne d’une compréhension humaine de ceux-ci, et a proposé de financer des mathématiciens afin qu’ils contribuent à donner à ces résultats une véritable signification scientifique.
Un écart entre le langage naturel et le code Lean
Les modèles commencent généralement par produire une explication en langage naturel, puis tentent de la convertir en Lean, un langage de programmation dont le compilateur peut confirmer la cohérence de la preuve dans un format exécutable. Toutefois, la conversion automatique peut modifier le contenu de la preuve ou créer un décalage entre ce que dit l’explication et ce que démontre le code.
Un article publié par des mathématiciens de l’université de Cambridge et du King’s College de Londres a relevé au moins deux différences entre une preuve en langage naturel et le code Lean associé à une solution fournie par OpenAI pour un problème dérivé des équations de Navier-Stokes concernant le comportement des fluides complexes. Ces différences ne prouvent pas nécessairement que l’une ou l’autre des solutions est erronée, mais elles soulèvent des doutes quant au fait de laisser les modèles formaliser eux-mêmes leurs solutions sans intervention humaine.
AGMAI a également demandé l’inclusion de métadonnées lisibles par machine établissant un lien entre la preuve textuelle et sa version formelle, ce qu’OpenAI n’a pas fourni dans ces publications. Les auteurs de l’article, connu sous le nom de « lost in translation », ont conclu que les preuves textuelles et les preuves Lean converties automatiquement ne devraient pas être acceptées par principe sans une évaluation par les pairs et un examen comparables à ceux auxquels sont soumises les autres preuves.
Pourquoi cette information est-elle importante ?
Le problème ne consiste pas seulement à démontrer que le code se compile avec succès, mais à établir que le code représente effectivement l’idée mathématique expliquée par le texte. Dans la recherche traditionnelle, les scientifiques assument la responsabilité de leurs résultats et les discutent au moyen d’articles, de conférences et de séminaires, un processus qui contribue à détecter les erreurs et à comprendre les méthodes réutilisables.
En revanche, lorsque les modèles produisent une solution à un problème difficile, cette compréhension humaine peut ne pas être disponible au moment de la publication. Les résultats actuels d’OpenAI semblent donc davantage constituer le début du processus de vérification scientifique que la fin du problème ; l’examen humain et la mise en relation des sorties textuelles et formelles restent deux conditions non résolues avant l’adoption de ces preuves au sein de la communauté mathématique.