Lean4 aide à découvrir un petit bug dans un récent article de Terence Tao
(mathstodon.xyz/@tao)- Terence Tao a découvert une erreur petite mais non triviale dans un article alors qu’il travaillait sur un projet de formalisation Lean4
- L’erreur est apparue dans l’argumentation de la page 6 de l’article arXiv
2310.05328, où1/2 log((n - 1)/(n - k - 1))diverge pourn = 3, k = 2 - Le problème est limité aux petites valeurs de
n: pourn >= 8, l’argument existant fonctionne, et les petitsnpeuvent être traités directement par une méthode plus grossière - Lean demandait une preuve de
0 < n - 3, mais la seule hypothèse étaitn > 2, si bien que la tactiquelinarithne parvenait pas à obtenir la contradiction nécessaire - Tao prévoit de corriger l’argument en ajustant certaines constantes numériques, et d’ajouter dans la nouvelle version une note indiquant que l’imprécision de l’argument précédent a été découverte lors de la tentative de formalisation avec Lean
Une erreur révélée par la formalisation Lean4
- Terence Tao a découvert, au cours de son projet de formalisation Lean4, qu’un article contenait un bug petit mais non trivial
- La formalisation visait l’argumentation de la page 6 de l’article arXiv
2310.05328 - L’expression en cause avait la forme suivante
1/2 log((n - 1)/(n - k - 1))
- Cette expression diverge dans le cas
n = 3, k = 2
Portée de l’erreur et méthode de correction
- Ce problème ne se produit que pour les petites valeurs de
n- pour
n >= 8, l’argument reste valable - les petits
npeuvent être traités directement par une méthode plus grossière, mais avec des constantes moins favorables
- pour
- Tao estime qu’il peut corriger l’argument en modifiant certaines constantes numériques de cette page
- Il prévoit aussi d’ajouter dans la nouvelle version de l’article une note de bas de page indiquant que l’argument précédent était légèrement imprécis et que cela a été découvert en essayant de le formaliser avec Lean
Le point précis où Lean a bloqué
- Au point où la formalisation a échoué, Lean demandait de prouver
0 < n - 3- la seule hypothèse disponible était
n > 2 - la tactique
linarithne parvenait pas à déduire une contradiction à partir de la négation de0 < n - 3
- la seule hypothèse disponible était
1 commentaires
Commentaires Hacker News
Il a commencé à apprendre Lean4 avec l’aide de GPT-4 au début du mois : https://mathstodon.xyz/@tao/111208692505811257
Une bonne partie de ses publications Mastodon ce mois-ci portaient sur ses progrès d’apprentissage, et c’est un exemple intéressant de la manière dont les grands modèles de langage peuvent accélérer même le travail de personnes au plus haut niveau
Fait intéressant, ce type d’outil pourrait aussi accroître les inégalités s’il n’est exploité efficacement que par des personnes très qualifiées
Si vous voulez découvrir Lean4 facilement, Natural Number Game est très bien : https://adam.math.hhu.de/#/g/hhu-adam/NNG4
Si vous préférez simplement lire sans passer par le jeu, c’est ici : https://lean-lang.org/theorem_proving_in_lean4/introduction.html
Au début, j’avais écrit Alloy « Allow »
Il y a quelques années, en cherchant un moyen de réduire les erreurs dans les programmes que j’écrivais, j’ai découvert TLA+ de Lamport, et j’ai appris à rédiger des spécifications formelles en pensant le comportement des programmes comme des machines à états
TLA+ m’a aidé à comprendre clairement les abstractions, puis j’ai aussi découvert la série Software Foundations, qui utilise l’assistant de preuve Coq pour construire des logiciels formellement corrects. Les exercices sont conçus comme de petits jeux, et je les ai trouvés assez agréables à résoudre : https://softwarefoundations.cis.upenn.edu/
Les spécifications formelles, abstraction de haut niveau, se concentrent sur un langage dédié pour décrire le code, tandis que les contrats de code, abstraction de plus bas niveau, reviennent plutôt à remplacer la logique de vérification par un meilleur modèle. C# a un temps eu Code Contracts[1], une approche simple mais puissante qui vérifiait les contrats à la compilation avec le solveur SMT Z3[2], mais le projet a été abandonné quelques années plus tard[3], puis retiré de .NET Runtime, ce qui y a mis fin de fait. Aujourd’hui, ce qui s’en rapproche le plus en C# est probablement Dafny[4], et côté développement de C#, on réfléchit encore à la manière de l’intégrer directement au langage[5]
[1] https://www.microsoft.com/en-us/research/project/code-contracts/
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Idris2 semble viser un langage généraliste tout en offrant un système de types plus avancé pour la preuve de théorèmes : https://github.com/idris-lang/Idris2
Il existe aussi un livre en partie dérivé qui utilise Agda au lieu de Coq : https://plfa.github.io/
Je ne l’ai pas encore lu, mais il est dans ma liste, et je pense qu’Agda ou Idris ont de bonnes chances de ressembler davantage à des langages de programmation que Coq
Les types dépendants me donnent vraiment envie. Cela dit, il y a peu de chances qu’ils arrivent à court terme
Dependent Haskell est en cours, mais il semble difficile de les greffer après coup dans un langage existant, et le créateur d’Idris disait espérer qu’Idris serve de modèle à d’autres langages, sans que son adoption grand public paraisse probable. Coq, Agda et F* n’ont pas non plus été conçus comme des langages généralistes. L’implémentation du compilateur est complexe et la syntaxe peut devenir verbeuse, mais ce que je veux, c’est la simplicité. Je veux encoder tout ce que je sais des entrées et des sorties. Dans les langages dominants actuels, on en sait souvent plus sur les arguments ou les sorties que ce que le système de types permet d’exprimer
J’aimerais une approche progressive, comme TypeScript, où l’on pourrait ajouter à n’importe quel endroit des informations de restriction de valeurs au niveau des types sans devoir tout prouver partout
Par exemple, si l’on connaît à la fois une liste de nombres et sa longueur, les types dépendants permettent de créer un type de liste qui inclut explicitement cette longueur, et de garantir à la compilation que les opérations respectent cette longueur. Si une fonction est définie pour n’accepter que des listes de longueur 3 et qu’on lui passe une liste de longueur 4, cela ne compile pas, ce qui permet de détecter l’erreur avant l’exécution. C’est comme une couche supplémentaire de vérifications de sécurité qui rend les types plus expressifs et permet même d’encoder des relations complexes entre variables
Si l’un des plus grands esprits de notre génération peut élargir son champ de travail grâce à la combinaison de grands modèles de langage et de démonstration automatique, l’avenir de cette combinaison technologique semble très prometteur.
Ça commence par la correction de bugs, puis par l’aide à la vérification, et au final cela poussera sans doute vers de nouvelles découvertes et repoussera les limites. Il faudrait un terme pour désigner le phénomène par lequel une dynamique à la loi de Moore « infecte » des domaines qui, à l’origine, n’avaient pas cette propriété cumulative. Pour ajouter du contexte, Terence Tao utilise Copilot pour apprendre Lean : https://mathstodon.xyz/@tao/111271244206606941
Il aurait probablement pu le faire sans Copilot, mais il ne se serait peut-être pas lancé à cause de la friction liée à l’adoption d’un nouvel outil. Les grands modèles de langage ont un fort potentiel dans ce type de situation de « bicyclette pour l’esprit ».
Il y a quelques années, j’avais aussi trouvé un bug dans un billet du blog de maths de Terence Tao. Je le lui ai signalé, il l’a corrigé et m’a remercié.
Évidemment, ça n’a pas fini en une de Hacker News.
Je craignais que Lean4 soit encore un autre grand modèle de langage, mais en réalité c’est un outil assez robuste et fiable.
Je me demande s’il serait possible de combiner des vérificateurs de preuves formelles comme le vérificateur de preuves Lean avec des modèles de langage qui génèrent des paires conjecture-preuve synthétiques dans un langage formel comme Lean.
Le vérificateur de preuves Lean pourrait vérifier automatiquement si les preuves synthétiques écrites par le modèle de langage sont correctes, et cette information pourrait servir de signal de récompense en apprentissage par renforcement appliqué au modèle de langage d’origine, afin de l’amener à produire de meilleures preuves. Ou bien on pourrait entraîner un nouveau modèle en utilisant comme données d’apprentissage les preuves synthétiques correctes des tours précédents. On pourrait aussi rendre le dispositif plus adversarial. On le séparerait en un modèle de génération de conjectures et un modèle de preuve/réfutation, puis on ajouterait un modèle qui prédit si une preuve synthétique sera validée par le vérificateur de preuves Lean. Plus la probabilité de bonne réponse est prédite comme faible, plus le modèle générateur de preuves recevrait une grande récompense lorsqu’il produit effectivement une preuve correcte. Enfin, si l’on ajoute un modèle qui prédit la récompense que recevra le modèle générateur de preuves pour une conjecture synthétique donnée, le modèle générateur de conjectures serait récompensé pour produire des conjectures dont la récompense attendue est élevée, ni trop difficiles ni trop faciles pour le modèle générateur de preuves. L’ensemble du système pourrait produire des preuves synthétiques de plus en plus difficiles, ce qui mènerait à un meilleur auto-apprentissage du modèle générateur de preuves. En principe, cela pourrait aller jusqu’à des capacités surhumaines en génération de preuves, de façon similaire aux GAN ou à l’auto-jeu d’AlphaGo Zero. La partie difficile est le bootstrapping initial : l’entraînement initial du modèle générateur nécessite des données de preuves Lean fournies par des humains. Mais une fois que les preuves synthétiques deviennent suffisamment bonnes, le système peut poursuivre automatiquement son auto-apprentissage
Au bout du compte, on pourrait obtenir un modèle qui connaît tous les théorèmes et toutes les preuves correctes de la littérature mathématique
Parmi les premières étapes consistant à démarrer par un apprentissage supervisé sur des preuves existantes puis à chercher de nouvelles preuves, on trouve TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms), entre autres. La plupart intègrent une forme de modèle de langage, mais si l’on cherche les grands modèles de langage qui ont récemment beaucoup attiré l’attention, il y a GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910) et COPRA (https://arxiv.org/abs/2310.04353). Cela dit, pour l’instant, ces modèles ne semblent pas aussi efficaces que les outils spécialisés qui ne sont pas de grands modèles de langage. Du côté de l’apprentissage par renforcement au-delà des preuves écrites par des humains, on trouve TacticZero (https://openreview.net/forum?id=edmYVRkYZv), l’article d’OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), les travaux de la famille HOList (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491), ainsi que des travaux en cours menés par l’équipe de l’University of Massachusetts et moi-même
Le contexte précédent sur la manière dont Tao a utilisé, dans ce parcours, des outils de grands modèles de langage, dont GPT-4, se trouve ici : https://mathstodon.xyz/@tao/111233986893287137
On peut aussi suivre son avancement sur GitHub : https://github.com/teorth/symmetric_project/