Je ne le suis pas plus, mais il ne faut pas pour autant être impressioné par ce qu'il s'est passé.
Avec sa remarque, BAud m'a donné le moyen d'expliquer simplement ce qui a eu lieu, et si cela peut sembler impressionnant, il faut relativiser.
La preuve automatique de théorèmes par un ordinateur cela n'a rien de nouveau, et c'est le quotidien de tous les utilisateurs d'une distribution Linux.
Tu veux installer firefox, tu conjectures que tu le peux, il y a deux cas :
l'installation marche, ta conjecture s'est avérée exacte ;
l'installation échoue, il y a des conflits, tu es réfutée.
Dans le cas de problème de la distance unitaire, on s'est retrouvée dans le second cas, voilà ce qui s'est passé. Le LLM a construit un contre-exemple, tout comme ton gestionnaire (apt ou un autre) a trouvé des conflits : les conflits qu'il explicite sont ses contre-exemples.
Dans le cas des gestionnaires de paquets, on se retrouve dans du NP-complet, c'est compliqué mais parfaitement décidable.
Dans le cas mathématique général, le procédé de recherche de preuves ou de réfutations est indécidable : c'est ce qu'ont montré Gödel et Turing. Comme le dit Martin-Löf dans sa conférence, pour parler le langage de Kant, avec un problème SAT (NP complet, le cas des gestionnaires de paquets) on est dans de l'analytique, tandis que le cas général des énoncés mathématique (dont la conjecture d'Erdös) est celui du synthétique a priori qui est indécidable. Il faut alors trouver d'autres méthodes pour y arriver, et c'est là qu'entre en jeu les méthodes formelles.
Pour l'industrie, on trouve par exemple :
- alt-ergo par l'équipe qui développe aussi opam le gestionnaire de paquets pour OCaml ;
- why3 qui est semi-automatique, certaines sont renvoyées vers Rocq pour un traitement manuel ;
- la méthode B qui fait fonctionner les métros automatiques de Paris.
Ce n'est pas un domaine inexploré de l'informatique, loin de là, ce sont mêmes ces questions, issues des mathématiques pures, qui font que nous avons aujourd'hui des ordinateurs. Mais personne au monde n'est venu affirmé que les machines étaient intelligentes grâce à cela et c'est incommensurablement plus fiable que n'importe quel perroquet stochastique. Gerard Berry qui a occupé la chaire au Collège de France avant Xavier Leroy, qui a fait toute sa carrière dans ce domaine de recherche, n'a jamais cessé de répéter qu'un ordinateur étant complément con : il calcule a une vitesse qui écrase tout être humain, mais il est con comme un balai.
Si l'on prend la méthode B, on peut faire ce titre racoleur : des millions de personnes de part de le monde voyage dans de métros automatiques grâce a des conjectures prouvées ou réfutées automatiquement (ou semi-automatiquement) par un ordinateur... sauf le Collège de France. ;-)
Jean-Raymond Abrial, l'inventeur de la méthode, a donné une conférence sur le sujet au Collège de France, invité par Gérard Berry. Je ne l'ai pas trouvé avec une rapide recherche, mais je suis sûr qu'elle existe, si quelqu'un est motivé.
Pour faire fonctionner la ligne 14 à Paris, les ingénieurs qui l'on conçu ont fait comme Erdös : de la formalisation et de la conjecture, et la machine se charge de confirmer ou d'infirmer leur intuition.
Néanmoins, dans le cas du métro automatique (comme pour un gestionnaires de paquets), on n'est pas intéressé par le contenu de la preuve elle-même. Si cela produit un gloubi boulga, on s'en fout, on veut juste la réponse mais avec la certitude que la machine ne se trompe pas (donc exit les perroquets). Par contre si l'on cherche une preuve formelle, que son contenu est ce qui nous importe le plus (cas des mathématiques pures ou même de la programmation usuelle, c'est la même chose par Curry-Howard), on envoie à la poubelle le code AI slop parce que son API est tout a chier et sans intérêt. D'où la réaction de Patrick Massot :
I think the situation is pretty clear: AI companies, and especially Math Inc, will indeed thoroughly bomb this area to turn it into a giant radioactive wasteland that will never be able to sustain life again, so we will never get the benefits expected from formalization (improved understanding and accessibility). I strongly advise young people to contribute to less shiny projects that are less likely to be destroyed.
Et je rajoute : quel est donc le projet politique de ces entreprises de la big tech pour vouloir jouer à ce jeu là ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . En réponse au lien Commentaire de gro-tsen sur la vidéo de Mr phi sur la résolution par LLM du problème de la distance unitaire. Évalué à 2 (+0/-0).
Je ne le suis pas plus, mais il ne faut pas pour autant être impressioné par ce qu'il s'est passé.
Avec sa remarque, BAud m'a donné le moyen d'expliquer simplement ce qui a eu lieu, et si cela peut sembler impressionnant, il faut relativiser.
La preuve automatique de théorèmes par un ordinateur cela n'a rien de nouveau, et c'est le quotidien de tous les utilisateurs d'une distribution Linux.
Tu veux installer
firefox, tu conjectures que tu le peux, il y a deux cas :Dans le cas de problème de la distance unitaire, on s'est retrouvée dans le second cas, voilà ce qui s'est passé. Le LLM a construit un contre-exemple, tout comme ton gestionnaire (
aptou un autre) a trouvé des conflits : les conflits qu'il explicite sont ses contre-exemples.Dans le cas des gestionnaires de paquets, on se retrouve dans du NP-complet, c'est compliqué mais parfaitement décidable.
Dans le cas mathématique général, le procédé de recherche de preuves ou de réfutations est indécidable : c'est ce qu'ont montré Gödel et Turing. Comme le dit Martin-Löf dans sa conférence, pour parler le langage de Kant, avec un problème SAT (NP complet, le cas des gestionnaires de paquets) on est dans de l'analytique, tandis que le cas général des énoncés mathématique (dont la conjecture d'Erdös) est celui du synthétique a priori qui est indécidable. Il faut alors trouver d'autres méthodes pour y arriver, et c'est là qu'entre en jeu les méthodes formelles.
Pour l'industrie, on trouve par exemple :
- alt-ergo par l'équipe qui développe aussi opam le gestionnaire de paquets pour OCaml ;
- why3 qui est semi-automatique, certaines sont renvoyées vers Rocq pour un traitement manuel ;
- la méthode B qui fait fonctionner les métros automatiques de Paris.
Ce n'est pas un domaine inexploré de l'informatique, loin de là, ce sont mêmes ces questions, issues des mathématiques pures, qui font que nous avons aujourd'hui des ordinateurs. Mais personne au monde n'est venu affirmé que les machines étaient intelligentes grâce à cela et c'est incommensurablement plus fiable que n'importe quel perroquet stochastique. Gerard Berry qui a occupé la chaire au Collège de France avant Xavier Leroy, qui a fait toute sa carrière dans ce domaine de recherche, n'a jamais cessé de répéter qu'un ordinateur étant complément con : il calcule a une vitesse qui écrase tout être humain, mais il est con comme un balai.
Si l'on prend la méthode B, on peut faire ce titre racoleur : des millions de personnes de part de le monde voyage dans de métros automatiques grâce a des conjectures prouvées ou réfutées automatiquement (ou semi-automatiquement) par un ordinateur... sauf le Collège de France. ;-)
Jean-Raymond Abrial, l'inventeur de la méthode, a donné une conférence sur le sujet au Collège de France, invité par Gérard Berry. Je ne l'ai pas trouvé avec une rapide recherche, mais je suis sûr qu'elle existe, si quelqu'un est motivé.
Pour faire fonctionner la ligne 14 à Paris, les ingénieurs qui l'on conçu ont fait comme Erdös : de la formalisation et de la conjecture, et la machine se charge de confirmer ou d'infirmer leur intuition.
Néanmoins, dans le cas du métro automatique (comme pour un gestionnaires de paquets), on n'est pas intéressé par le contenu de la preuve elle-même. Si cela produit un gloubi boulga, on s'en fout, on veut juste la réponse mais avec la certitude que la machine ne se trompe pas (donc exit les perroquets). Par contre si l'on cherche une preuve formelle, que son contenu est ce qui nous importe le plus (cas des mathématiques pures ou même de la programmation usuelle, c'est la même chose par Curry-Howard), on envoie à la poubelle le code AI slop parce que son API est tout a chier et sans intérêt. D'où la réaction de Patrick Massot :
Et je rajoute : quel est donc le projet politique de ces entreprises de la big tech pour vouloir jouer à ce jeu là ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.