IA et math un bond en avant?

Boécien

La lecture de cet article semble le suggérer.

philou22

@Boécien Une seule question, est-ce que l’IA a déjà résolu ne serait-ce qu’un seul problème de mathématiques non résolu pendant plus d’une semaine par la communauté des mathématiciens ? J’ai déjà entendu quelqu’un dire que l’IA allait décrypter RSA… L’IA n’est « que » l’alliage des statistiques et de l’informatique, ce n’est pas une avancée scientifique majeure mais l’évolution naturelle de l’informatique. Elle est impressionnante car les ressources nécessaires à son développement deviennent abondamment disponibles (données, puissance de calcul, recherche fondamentale). Ce n’est pas la découverte de la radioactivité ou l’invention du transistor. Cependant j’admets qu’à son niveau actuel, elle accélère l’exploration de la « zone de développement proximal » de chacun avec une amplitude telle qu’il serait dommage de la négliger.

Dom

En effet, il faudrait savoir si l’IA pouvait résoudre un problème (même tout petit) mais disons « jamais » résolu. 

Moins naïvement, j’ai l’impression que l’IA peut donner des idées et non résoudre des choses problèmes « difficiles ». Car parfois, ce qu’il manque, ce n’est pas l’outil mathématique, mais la bonne idée pour avancer.

philou22

En effet, l’IA est souvent performante pour ne pas rester bloquée dans une boucle d’échecs et proposer une nouvelle approche raisonnable. Elle reste cependant parfois elle aussi bloquée dans une boucle d’échecs mais la collaboration humain-IA permet d’expérience de sortir des blocages. Au début l’humain n’a plus d’idées, souvent l’IA en a, lorsque l’IA bloque à son tour, l’humain trouve une nouvelle idée. C’est le petit retour d’expérience que j’ai dans la programmation de systèmes complexes en collaboration avec une IA.

Seirios

Voici une vidéo proposée par Quanta Magazine, qui me semble être dans le thème de la discussion : How AI discovered a faster matrix multiplication algorithm. 

Boécien

Merci pour le lien vers cette vidéo. On espère tous que l'IA et les logiciels de vérification de preuve (j'ai découvert récemment l'incroyable puissance de Walnut en combinatoire des mots) auront besoin d'être couplés à l'humain dans une démarche d'analyse-synthèse (guessing and check en anglais) pour démontrer des conjectures compliquées qu'il est quasi impossible de prouver à la main. L'humain conjecture et l'IA et les logiciels prouvent. Mais j'ai le sentiment que ça ne va pas durer et que bientôt certaines IA sauront faire des conjectures intuitives non triviales.

lourrran

Le premier lien donné par Boécien nous dit que l'IA a résolu le problème 'cap set' pour des grands nombres de points, alors que les mathématiciens n'y arrivaient pas.

Dom

J’ai jeté un œil à ce problème. 

Avec une machine qui travaille vite, si j’ai bien compris, un humain peut y parvenir en examinant tous les cas (enfin… en les faisant examiner…). 

Mais là, quand on parle IA, s’agit-il alors de « vraie preuve » ou bien d’essais faits par la machine ?

lourrran

De ce que je comprends de l'article, la solution proposée par l'IA est générique. Un humain va trouver une solution pour le cas n=40, puis il va repartir de 0 pour le cas n=41etc etc, et la solution proposée par l'IA serait valable pour tout n.
Mais restons sceptique.
Dans un domaine autre et que je connais bien, j'ai vu il y a 2 ans environ des communications enthousiastes sur une IA qui avait une performance extraordinaire. Il se trouve que j'avais suivi le protocole de l'expérience de près, et clairement, la réalité était beaucoup moins belle que ce les communicants disaient. 
Pour lever des fonds, et pour plein d'autres raisons, les communicants embellissent fortement la réalité.

Sylvain

Je serais curieux de voir ce que donnerait une IA guidée par des principes fondamentaux comme l'inspirante citation de Weyl "pour comprendre un objet mathématique, il faut étudier le groupe de ses automorphismes" lue sur le site il y a des années.

Chalk

@Seirios
Juste pour info ce n'est pas de l'IA générative et ce n'est même pas certain que ce soit de l'IA, ça se rapproche beaucoup de l'optimisation relaxée (de mémoire quand j'avais lu le papier de recherche). En tout cas le modèle est très hard codé car on sait exactement ce qu'on cherche à faire.

biguine_equation

Pour réduire le nombre d’étapes dans la multiplication des matrices, AlphaTensor utilise l’apprentissage profond (« Deep Reinforcement Learning »). 

Il est proposé à la machine un (auto)-jeux qui consiste à trouver le plus court chemin entre le tenseur de la matrice de multiplication et le tenseur zéro. C’est le « Tensor decomposition game ».
AlphaTensor est entraîné avec des algorithmes connus comme celui de Strassen sur différents corps comme $\mathbb{F}_2$ et différentes tailles de matrices. Il aurait ainsi trouvé plus de 14 000 algorithmes de réduction pour les matrices $4 \times 4$. On n’en connaissait qu’un avant l’IA (celui de Strassen).

Voir la vidéo: AlphaTensor, discover faster matrix multiplication algorithme with RL-Matej Balog. Fascinant ! Abstraction faite du petit laïus nous assurant que Google travaille pour le bien de l’humanité.