AlphaGO Zéro

[HenriParisien1]

Je suis vraiment très loin de ces trucs, mais mathlab ne fait pas déjà le job ?
-----

[minushabens]

mathlab ne fait pas déjà le job ?

non pas vraiment. Il y a des programmes qui font des démonstrations mathématiques mais jusqu'à présent aucun n'a démontré le conjecture de Riemann ni (à ma connaissance) aucun problème réellement difficile.

[Deedee81]

On a aussi d'excellent vérificateur de démonstration comme Coq.
Et des programmes spécifiques (effectivement implémenté dans les outils) parfois basé sur l'I.A. pour des problèmes spécifiques.
Mais je ne serais pas surpris si le deep learning pouvait faire mieux.
Je pense à des problèmes ouverts qu'on trouve un peu partout (j'en ai vu par exemple récemment en potassant la théorie des algèbres de Von Neumann, il y aussi certains problèmes de classement comme les variétés riemannienne ou même les variétés hyperboliques de courbure constante en 3D, ....)

Bon, je pense que pour un moment encore le génie humain ne sera pas surpassé dans ce domaine (imaginer des conjectures puissantes, imaginer de nouvelles structures mathématiques utiles,...). Mais ce serait quand même pas mal si des avancées pouvaient se faire.

[pm42]

En fait, on ne sait pas. Un chercheur en IA me disait récemment que le deeplearning fonctionne bien pour les domaines où le contenu sémantique est faible.
C'est le cas de la reconnaissance d'image, des jeux, du traitement "global" des textes (résumé, détection d'émotions).

Par contre, une démonstration mathématique contient et même crée un fort contenu sémantique.
Pour les vérificateurs formels comme Coq, ce qui fait leur valeur est le coté 100% rigoureux. Est ce que le deeplearning apporte vraiment quelque chose ?
On pourrait penser qu'il serait plus utile pour détecter des erreurs probables dans du code classique, écrit sans les contraintes de Coq.

[minushabens]

d'après ce que je comprends du "deep learning" (mais en fait je n'y comprends pas grand-chose) il fonctionne un peu comme le dressage d'un animal qui s'il réussit une certaine épreuve reçoit une récompense (un poisson si c'est une orque). Dans le cas de parties d'échecs l'épreuve est toujours la même et la récompense aussi (le mat).

Dans le cas des démonstrations mathématiques les épreuves se ressemblent plus ou moins et le succès n'est pas facile à établir. C'est pourquoi je demandais si c'était théoriquement possible d'utiliser cette méthodologie pour résoudre des problèmes mathématiques. Je ne posais pas la question de l'utilité d'une IA en général.

[HenriParisien1]

De ce que je comprends, le coté révolutionnaire d'AlphaGoZéro et d'AlphaZéro (mais pas d'AlphaGo), c'est l'aspect auto-apprentissage grâce au couplage avec algorithme alpha/béta.
Cet algo est quand même très spécifique aux jeux qui se jouent au tour par tour et n'est – sauf erreur de ma part – pas du tout adapté à des jeux en temps réels (comme starcraft). Pour généraliser AlphaZéro à d'autres problématiques, il faut trouver une technique qui puisse faire la même chose.

Mais quand même, en imaginant qu'il en existe une. On donne à un des successeurs d'AlphaZéro les axiomes de Peano, 4 heures après, il a trouvé tous ce que l'humanité à produit depuis qu'elle existe. Il produit de nouveaux résultats pendant 2 heures, et ensuite il nous dit : c'est bon, il n'y a plus rien à trouver !

Cette perspective est – à mon avis – bien plus terrifiante qu'un SkyNet.

[minushabens]

Je crois que si les machines faisaient des mathématique mieux que nous ça m'attristerait. D'un autre côté, les humains développent les mathématiques qui les intéressent et pas les autres. Les machines feraient sans-doute d'autres mathématiques et je serais curieux de voir ce qui les intéresse. A moins qu'elles se contentent de cracher des millions de formules parmi lesquelles se cacheraient quelques théorèmes intéressants?

[Bounoume]

A moins qu'elles se contentent de cracher des millions de formules parmi lesquelles se cacheraient quelques théorèmes intéressants?

C'est l'idée que j'avais il y a longtemps, quand on avait une base de faits, une base de règles, et Prolog....
Si il en est encore ainsi, pas facile de découvrir LA proposition nouvelle et fondamentale (et combien de temps d'évaluations de résultats inutiles avant?)

[Deedee81]

SAlut,

En fait, on ne sait pas. Un chercheur en IA me disait récemment que le deeplearning fonctionne bien pour les domaines où le contenu sémantique est faible.
C'est le cas de la reconnaissance d'image, des jeux, du traitement "global" des textes (résumé, détection d'émotions).

Ah oui, c'est une remarque sacrément pertinente. J'avoue ne pas du tout y avoir pensé.

Je suppose que certains progrès seront obtenus en combinant des technologies orthodoxes avec du deep learning.

c'est bon, il n'y a plus rien à trouver !

Ca me rappelle Monsieur Gru (Moi moche et méchant) à l'école quand il dit qu'il veut devenir explorateur. Et l'institutrice rembobine la carte au mur en disant "trop tard, on a déjà tout exploré"

Cette perspective est – à mon avis – bien plus terrifiante qu'un SkyNet.

Heu, faudrait revoir tes priorités
Je suppose que tu voulais dire "plus probable qu'un SkyNet" (et sacrément déprimante évidemment, le pire étant que je suis informaticien et que je me dit : mais qu'on on est concombre, on scie la branche sur laquelle on est assis)

[HenriParisien1]

Heu, faudrait revoir tes priorités
Je suppose que tu voulais dire "plus probable qu'un SkyNet" (et sacrément déprimante évidemment, le pire étant que je suis informaticien et que je me dit : mais qu'on on est concombre, on scie la branche sur laquelle on est assis)

Elles sont dans le "bon" ordre. Un SkyNet nous donne un rôle : on doit le combattre.
Une machine qui - en quelques heures - résout tous les problèmes mathématiques ne nous en donne plus aucun. On devient les chats de nos IA (un peu comme dans la Culture de Banks).

--

Bon cette digréssion terminée et pour rester dans le domaine spéculatif. Si on découvre un moyen universel de permettre à des IA de rentrer dans des boucles d’auto apprentissages, cette histoire de "terminer" les mathématiques ne parait absolument pas impossible. Après tout, il n'y a guère que les mathématiques qui n'ont pas la nécessité d'une rétroaction avec le monde physique (même si pas mal de problème mathématique ont pour origine des problèmes pratiques).

Dès qu'on part sur des sciences appliqués (physique, biologie, sciences humaines) on a besoin d'expérience pour discriminer les hypothèses. Et une IA - aussi forte qu'elle soit - ne pourra jamais construire un collisionneur de particules en quelques heures

[Deedee81]

Elles sont dans le "bon" ordre. Un SkyNet nous donne un rôle : on doit le combattre.
Une machine qui - en quelques heures - résout tous les problèmes mathématiques ne nous en donne plus aucun. On devient les chats de nos IA (un peu comme dans la Culture de Banks).

On peut toujours jeter le résultat et dire "m'en fout, je veux trouver moi-même".

Ou comme dans l'anecdote que j'avais lue sur les difficultés dans le domaine mésoscopique (ou le quantique doit être pris en compte mais les calculs souvent irréalisables vu la complexité).
Suite à un problème avec la conception d'un système avec des puits quantiques and so on, les physiciens avaient programmé un ordinateur pour calculer les résultats.
Tout fier, ils montrèrent les résultats à l'ingénieur. Celui-ci répondit, "formidable, l'ordinateur a compris. Maintenant j'aimerais bien comprendre, moi aussi."

[pm42]

Dès qu'on part sur des sciences appliqués (physique, biologie, sciences humaines) on a besoin d'expérience pour discriminer les hypothèses. Et une IA - aussi forte qu'elle soit - ne pourra jamais construire un collisionneur de particules en quelques heures

Cela me semble rapide. On ne sait pas ce qu'un IA forte serait capable de faire notamment par le calcul, la simulation, etc.
Si elle était capable de performances comparables à AlphaZéro, elle pourrait très bien avoir un besoin limité d'expériences ou être capable de concevoir des moyens efficaces auxquels nous n'avons pas pensé.

[HenriParisien1]

Bien sur que c'est rapide : Mais si on ne sait pas ce qu'un IA pourrait faire, on sait que nous nous ne pouvons pas faire.
Et en particulier, trouver des phénomènes totalement inconnu via la simulation, comme par exemple la supra conductivité à haute température.

Et je ne pense pas que pour rester à des expériences vieille d'un siècle, on n'est des moyens plus simple de montrer l’invariance de la vitesse de la lumière que l’expérience initiale de Michelson-Morley ou la rotation de la terre que le pendule de foucault

[JPL]

Tout fier, ils montrèrent les résultats à l'ingénieur. Celui-ci répondit, "formidable, l'ordinateur a compris. Maintenant j'aimerais bien comprendre, moi aussi."

Exactement la question qu’on se pose pour certains diagnostics ou prescriptions médicales par "intelligence" artificielle. Un médecin est toujours capable d’expliquer son choix, même imparfait, mais pas ces monstres informatiques dont leurs créateurs ne savent même pas ce qui s’y passe.

[HenriParisien1]

Exactement la question qu’on se pose pour certains diagnostics ou prescriptions médicales par "intelligence" artificielle. Un médecin est toujours capable d’expliquer son choix, même imparfait, mais pas ces monstres informatiques dont leurs créateurs ne savent même pas ce qui s’y passe.

Attention, la plupart des médecins sont capable de donner une explication "convaincante" de leurs choix. Mais une explication "convaincante" n'est pas forcément la "bonne" - au sens exacte scientifiquement - explication. Et en pratique comprendre exactement une explication technique suppose d'avoir le même niveau de connaissance que l'expert au moins sur le sous-domaine considéré.

Pour la plupart des décisions "techniques" qui ne sont pas de nos domaines de compétences, on s'en remets à l'avis des experts parce qu'ils ont souvent raison. Si les IA ont - à leur tour - souvent raisons, je ne vois aucune raison pratiques à ce que nous ne leur fassions pas confiance.

[JPL]

Sauf que s’agissant de la vie des personnes, si ce que recommande l’IA est en contradiction avec ce que recommandent un ou plusieurs spécialiste il y a une obligation d’éthique forte pour justifier, donc expliquer, son choix.

[HenriParisien1]

Bien sûr. Tout comme si un spécialiste d'un domaine préconise un choix contraire au consensus de ses paires, il doit préparer une solide argumentation pour le défendre. Mais je crois que ce forum n'est pas le meilleur endroit pour discuter de l'acceptation sociale des avis des IA. Puisque c'est un peu de ça dont nous parlons depuis quelques échanges.

--

Mais je voulais juste revenir sur cette histoire de preuve d'IA. Ici, il y a une nouvelle "prouesse" des IA : http://www.lefigaro.fr/sciences/2017...eme-etoile.php

En pratique, on se moque un peu (*) de la façon dont l'IA a trouvé qu'il y avait une nouvelle planète. Il nous suffit qu'elle nous ait dit :"Hé, regardez-la, j'ai trouvé une nouvelle planète". Et du coup, on regarde et on vérifie qu'il y a bien une nouvelle planète.

Si une IA médicale dit "Hé, mais il y a une tumeur sur ce scanner", et bien on la passe à des spécialistes, et ils vont dire : "Ah ben oui, il y a une tumeur, ou non faux signal". L'avantage c'est qu'on a une détection automatique et systématique et qu'on limite ainsi la simple fatigue qui fait qu'un spécialiste - aussi consciencieux qu'ils soit - puisse louper un diagnostic. Après, avec le temps, si à chaque fois que l'IA dit "Hé, mais il y a une tumeur sur ce scanner", il y a bien une tumeur, et bien les spécialistes perdront leur job.

--
(*) sauf bien sûr si on est un spécialiste de l'IA.

[JPL]

Bien sûr. Tout comme si un spécialiste d'un domaine préconise un choix contraire au consensus de ses paires

Je ne demande jamais l’avis de ma paire... de mes pairs à la rigueur

[pm42]

mais pas ces monstres informatiques dont leurs créateurs ne savent même pas ce qui s’y passe.

C'est justement un axe de recherche actif : soit d'utiliser des techniques différentes que le deeplearning, soit de trouver une façon de comprendre comment les réseaux de neurones arrivent à leur conclusion.
Et c'est justement pour qu'on puisse s'en servir dans des cas où il faut être capable d'expliquer la conclusion.
Il faudrait que je retrouve des références mais là, je manque un peu de temps.

[minushabens]

Exactement la question qu’on se pose pour certains diagnostics ou prescriptions médicales par "intelligence" artificielle. Un médecin est toujours capable d’expliquer son choix, même imparfait, mais pas ces monstres informatiques dont leurs créateurs ne savent même pas ce qui s’y passe.

effectivement si on arrive à appliquer la méthodologie de deep learning à la démonstration de conjectures mathématiques, une possibilité est que la machine réponde au bout d'un certain temps: j'ai montré que la conjecture de Riemann était correcte, je peux l'imprimer mais il me faudrait 10000 ramettes de papier, puis-je passer la commande?

[pm42]

Pas besoin de deeplearning. C’est déjà le cas avec certaines démonstrations assistées par ordinateur. C’est loin dans ma mémoire mais je crois que le théorème des 4 couleurs et la classification des groupes finis ne sont pas accessibles à un humain.

[JPL]

Dans le théorème des 4 couleurs on a demander à l’ordinateur d’éliminer tout un tas de solutions qu’il a trouvées fausses dans un temps raisonnable et quand le problème s’est restreint à un nombre abordable de configurations à étudier par un humain la démonstration a pu être faite par un raisonnement logique et non par la force brute de l’ordinateur. En gros c’est ce que j’ai retenu.

[ansset]

bonsoir,

Bien sûr. Tout comme si un spécialiste d'un domaine préconise un choix contraire au consensus de ses paires,....

j'ai pris ce début de phrase de manière indirecte , pour illustrer la remarque suivante.
dans ces derniers échanges, on évoque bien des capacités de diagnostics voire de décisions de spécialistes.
( évocation d jeux, de domaines spécifiques segmentés, ..)
On parle peu de capacités "multi dimensionnelles" ou des champs différents d'expertises complémentaires sont nécessaires (*), et ou il ne suffirait certainement pas d'attribuer des coeffs arbitraires en fonction de l'angle de vue considéré.
mais il se peut que je m'éloigne du sujet de ce fil que je n'ai fait que parcourir.

(*) c'est en partie l'exemple de la médecine citée plus haut qui m'amène à cette considération plus générale.

[minushabens]

Dans le théorème des 4 couleurs on a demander à l’ordinateur d’éliminer tout un tas de solutions qu’il a trouvées fausses dans un temps raisonnable et quand le problème s’est restreint à un nombre abordable de configurations à étudier par un humain la démonstration a pu être faite par un raisonnement logique et non par la force brute de l’ordinateur. En gros c’est ce que j’ai retenu.

c'est un peu plus compliqué mais effectivement un humain aurait pu s'il en avait eu le temps (s'il avait vécu quelques milliers de vies) faire les calculs qui ont été faits par l'ordinateur. Ce n'est pas à mon point de vue de l'intelligence artificielle. D'ailleurs la méthode a été décrite dans un article que j'ai lu et compris à l'époque (d'accord, un article de plus de 100 pages).

Je pensais à une démonstration formelle réellement impossible à comprendre par un humain. Une démonstration mathématique formelle est une suite de formules (une suite de chaînes de symboles, ou même une unique longue suite de symboles si l'on veut). L'enchaînement des formules suit certaines règles et on peut (facilement en principe) vérifier que les règles ne sont pas violées, mais ce n'est pas comme ça qu'un humain comprend une démonstration, il a besoin d'y mettre du "sens". J'ai peur qu'une démonstration produite par une IA ne produise pas de sens. Je crois que c'est plus ou moins ce que disait pm42.

[invite73192618]

En fait, on ne sait pas. Un chercheur en IA me disait récemment que le deeplearning fonctionne bien pour les domaines où le contenu sémantique est faible.
C'est le cas de la reconnaissance d'image, des jeux, du traitement "global" des textes (résumé, détection d'émotions).

Par contre, une démonstration mathématique contient et même crée un fort contenu sémantique.
Pour les vérificateurs formels comme Coq, ce qui fait leur valeur est le coté 100% rigoureux. Est ce que le deeplearning apporte vraiment quelque chose ?
On pourrait penser qu'il serait plus utile pour détecter des erreurs probables dans du code classique, écrit sans les contraintes de Coq.

Un peu hs, mais un truc qui serait sympa serait un traducteur Coq-language usuel et inversement.

[pm42]

Un peu hs, mais un truc qui serait sympa serait un traducteur Coq-language usuel et inversement.

Tu peux préciser ? Ma connaissance de Coq est très limitée.

[invite73192618]

Je n'y connais pas grand chose non plus. Tout ce que je sais c'est qu'actuellement on a des démonstrateurs automatiques comme Coq, mais que coder une preuve 'humaine' en preuve pouvant être vérifié mécaniquement semble un travail très spécialisé et apparement rébarbatif*. Pourtant ce pourrait être très utile, ne serait-ce que pour vérifier la myriade de démonstrations qui n'ont été validées que par une demi-douzaine de personnes. A l'inverse, un assistant logiciel qui peut expliquer une démonstration mécanique en français de tous les jours, c'est pas loin d'être un bon prof de math.

*Par exemple, à un moment donné j'ai cherché en vain une preuve Coq de la diagonale de Cantor**, qui est quand même très courte et très connue. Tout ce que j'ai trouvé c'est deux travaux étudiants de l'ENS: dans un l'étudiant disait qu'il n'avait pas fait cette démonstration mais que ce serait bien sur très facile à faire. Dans l'autre l'étudiant disait qu'il n'avait pas fait la démonstration parce que ce serait bien trop difficile.

**il en existe (au moins) une version naïve, très proche de celle qui est généralement acceptée, qui est fausse à cause de la non-unicité de l'écriture décimale. C'est réparable en s'arrangeant pour que le nombre diagonal ne puisse pas être écrit de deux façons, mais je n'ai jamais compris comment cette modification était reliée aux axiomes, d'où l'idée de regarder comment c'était implémenté dans une démonstration mécanique.

[invite73192618]

**il en existe (au moins) une version naïve, très proche de celle qui est généralement acceptée, qui est fausse à cause de la non-unicité de l'écriture décimale. C'est réparable en s'arrangeant pour que le nombre diagonal ne puisse pas être écrit de deux façons, mais je n'ai jamais compris comment cette modification était reliée aux axiomes, d'où l'idée de regarder comment c'était implémenté dans une démonstration mécanique.

Dans la même veine: la démonstration wikipedia passe partiellement à coté du problème. En effet elle stipule que le nombre diagonal 'x (...) ne peut pas être dans la suite ( r1, r2, r3, … ), car il n'est égal à aucun des nombres de la suite : il ne peut pas être égal à r1 car la première décimale de x est différente de celle de r1, de même pour r2 en considérant la deuxième décimale, etc.'.

Voici deux nombres qui diffèrent sur leur cinquième décimale mais qui sont bien égaux.
x=0.1111100000...
y=0.1111099999...

Bref ce n'est pour cela que x diffère de tous les r. Il diffère parce qu'au moins une décimale diffère ET que x n'admet pas deux écritures en décimal.

définitivement hs...

[pm42]

Ok. De mémoire (et ça ne vaut pas grand chose parce que ça remonte à loin et que je souffre de décalage horaire), on s'en sortait en construisant un nombre diagonal qui soit différent pour chaque décimale et qui ne contient ni 0 ni 9. Ce qui garantit l'unicité de son écriture et il n'est pas dans la liste par construction.

Mais on diverge. Pour un outil d'aide Coq -> Humain et Humain -> Coq, tu penses que ce serait faisable en deeplearning ?
Je me demande quelle serait la fiabilité.

D'ailleurs, une question que je me pose est de savoir si on peut entrainer un réseau à être rigoureux à 100% dans des domaines qui le nécessitent.

[invite73192618]

Pour un outil d'aide Coq -> Humain et Humain -> Coq, tu penses que ce serait faisable en deeplearning ?

Avec les techniques de deep learning 'standard' actuelles, ça m'étonnerait. Il y a une actu fs sur une nouvelle d'Harry Potter faite par IA qui montre bien l'état de l'art en écriture automatique: les phrases sont bonnes, le style est intéressant, mais la nouvelle est sans queue ni tête. Autrement dit on pourrait très probablement avoir une IA qui crache du code valide, mais pour des démonstrations qui ne vont nulle part, i.e. la compréhension de la démonstration serait absente.

Cela dit, cela dépend peut-être de ce que tu considères comme technique standard. Si on inclu une technique à la alphazero, on peut peut-être faire mieux. Un truc intéressant c'est que les assistants de démonstration pourrait servir d'évaluateur signalant les erreurs dans une game en self-play. ...mmm cela mérite réflexion