Un prof de Berkeley clôt avec GPT-5.6 Sol un problème de 1996

Un enseignant-chercheur en IEOR à UC Berkeley, Phillip Kerger, raconte sur Medium avoir refermé, avec l'aide de GPT-5.6 Sol, un écart théorique en optimisation convexe resté ouvert depuis 1996.

Le problème est technique mais bien connu du domaine. En optimisation convexe zeroth-order déterministe et possiblement non lisse, un algorithme de Protasov datant de 1996 fournit déjà une borne supérieure de l'ordre de d² évaluations de fonction. Mais la meilleure borne inférieure publiée depuis trente ans plafonnait à l'ordre de d, laissant un écart quadratique dont personne ne savait s'il pouvait être fermé du côté de l'algorithme ou du côté de la limite fondamentale. Le résultat annoncé par Kerger tranche dans le second sens : une borne inférieure de l'ordre de d², à des facteurs logarithmiques et constants près. Autrement dit, la méthode de Protasov serait essentiellement optimale.

Ce qui rend l'annonce intéressante ne se réduit pas à la borne. Kerger décrit un protocole précis : un prompt de dix pages soumis au modèle, deux heures et demie de génération sans aucune intervention de sa part, puis une vérification formelle de la démonstration dans Lean. « Sol 5.6 had solved the problem in one shot », écrit-il, avant de préciser que le contrôle Lean est passé. Ce couple modèle de raisonnement plus assistant de preuve change un peu la nature du risque intellectuel. On ne demande plus au lecteur de croire un chatbot, on lui propose de faire tourner un vérificateur qui ne pardonne pas une étape manquante.

La mise en garde honnête est qu'à ce stade, il s'agit d'un billet de blog d'un seul chercheur, accompagné d'un dépôt GitHub. Le texte ne détaille pas ce que dix pages de prompt ont effectivement injecté dans la construction, ne mentionne pas de passage en revue par les pairs, et ne dit rien sur la reproductibilité du protocole avec d'autres modèles ou d'autres énoncés. Il faut donc prendre le résultat pour ce qu'il est, une annonce sérieuse qui devra passer par la communauté d'optimisation.

Si ce type de flux se stabilise, l'effet de levier pour les petits laboratoires de mathématiques appliquées devient tangible. Un chercheur seul, un abonnement à un modèle de raisonnement et un vérificateur formel commencent à composer une pile qui, il y a peu, exigeait plusieurs post-doctorants et beaucoup de temps.