Désolé, Tom, mais ça y est, la prédiction de Samuel Butler dans Erewhon se réalise, l'Humanité est fichue, un Robot généticien fait sa première découverte "indépendante", en semblant suivre une méthode expérimentale à la Claude Bernard (Observation, Inférence, Test expérimental).
When you sequence the yeast genome - the 6,000 different genes contained in yeast - you know what all the component parts are, but you don't know what they do," explained Professor King.
The robot was able to work out the role of the genes by observing yeast cells as they grew.
It used existing information about the function of known genes to make predictions about the role an unknown gene might play in the cell's growth.
It then tested this by looking at a strain of yeast from which that gene had been removed.
(...)
"it's more like a junior lab assistant" than a scientist. "It will be a long time before computers can replace human scientists."
Voir aussi New Scientist :
To discover which genes coded for which enzymes, Adam cultured a mutant yeast with a certain gene knocked out, and monitored how well the mutant grew without a particular metabolite. If the strain grew poorly without the metabolite, Adam learned something about the function of the knocked out gene. The robot could carry out more than 1000 of these experiments a day.
In all, Adam formulated and tested 20 hypotheses about genes coding for 13 enzymes. Twelve hypotheses were confirmed. For instance, Adam correctly hypothesised that three genes it identified encode an enzyme important in producing the amino acid lysine. The researchers confirmed Adam's work with their own experiments.
The team is now working on a new robot, called Eve, which will search for new drugs.
Blog de Nature, Wired, Science Daily.
En logique et mathématique, des ordinateurs ont déjà aidé à prouver des théorèmes (par exemple Le théorème des 4 couleurs). Nqthm de Boyer-Moore a déjà (re-)prouvé mécaniquement des théorèmes déjà connus (dont le théorème de Gödel en 1986, ce qui est ironique quand on connaît l'usage que John Lucas avait essayé de faire du "Gödelisme" - ou de la "gödelite" comme disait Jean-Yves Girard). Mais à ma connaissance, il n'y a jamais eu encore de machines qui ont découvert de nouveaux théorèmes encore inouïs - peut-être parce que pour l'instant les efforts pour concevoir un ordinateur explorant par lui-même des structures comme les Groupes demanderait plus de temps que de les explorer directement ?
8 commentaires:
C'est le théorème des 4, et non 5, couleurs, qui a été prouvé à l'aide d'un ordinateur ! Et si les ordinateurs ne prouvent pas des théorèmes nouveaux, c'est d'abord parce qu'ils ne savent pas reconnaître un beau théorème, et aussi parce qu'explorer l'ensemble des théorèmes possibles informatiquement est extrêmement long : il faut (encore ?) une heuristique humaine pour se diriger dans cet espace des théorèmes possibles...
Merci, oui, 4, je corrige (et l'entrée dit que l'usage de l'ordinateur a créé des résistances pour accepter la preuve).
Mais est-ce qu'on pourrait bientôt en démonter au moins des tas de théorèmes "pas intéressants" même si l'heuristique humaine permet de saisir ce qui serait plus fécond ou plus élégant ?
@Phersv: à vrai dire, c'est déjà le cas dans au moins un domaine : la preuve de programme. Les propriétés concernant les programmes admettent en général des preuves assez simples, mais très fastidieuses parce qu'elles font intervenir des objets bien plus « gros » que ceux habituellement étudiés par les mathématiciens ; on a donc beaucoup à gagner en employant un prouveur automatique.
Ensuite, il faut bien distinguer les assistants de preuve, qui proposent au mathématicien de construire interactivement sa démonstration puis vérifient formellement la correction de cette dernière, et les prouveurs automatiques qui sont des programmes cherchant à démontrer le plus efficacement possible un théorème (souvent sans donner de preuve).
De façon peut-être paradoxale, ces deux disciplines se sont développées assez séparément, les assistants étant basés sur des systèmes inspirés de la théorie des types (qu'on peut faire remonter à Russel, évidemment, mais surtout à Per Martin-Löf) et les prouveurs automatiques sur diverses méthodes que je qualifierais d'« heuristico-sémantiques » (tableaux à la Hintikka, solveurs SAT, etc.).
Comme vous vous en doutez, beaucoup de recherche a été consacrée à l'intégration entre la puissance déductive du prouveur et la rigueur et interactivité de l'assistant, avec plus ou moins de succès. La démonstration du théorème des quatre couleurs, très calculatoire, repose de façon cruciale sur une famille de méthodes automatiques employable dans les assistants basés sur la théorie des types.
La France a vraiment une grande expertise en la matière ; l'assistant de preuve Coq est une, sinon la référence en la matière.
Pour un revenir à la question initiale, la plateforme Why développée au Laboratoire de Recherche en Informatique de Paris 11, conjugue joliment théorie de la programmation, preuve automatique et assistants. L'utilisateur annote son programme, écrit dans un langage de programmation ordinaire, avec les propriétés qu'il souhaite prouver ; le contexte « propriétés + code source » est traduit dans un format générique intelligible par un prouveur. Si jamais ce dernier échoue (propriété fausse ou preuve trop difficile), le logiciel passe la main à Coq pour que l'utilisateur prouve lui-même sa propriété.
Dans le même numéro, il y a aussi un papier de l'équipe de Hod Lipson (le spécialiste des robots que les media, le blogueurs et wired adorent) qui fait découvrir la notion d'hamiltonien à son ordinateur.
Je commenterai sûrement dans les jours qui viennent sur mon blog moi aussi, j'ai bondi de ma chaise et me suis arraché les cheveux quand j'ai vu ces deux papiers. Je trouve qu'ils sont très symptomatiques de certaines dérives de la science et de Science, la revue...
@Tom Roud: tout cela me rappelle les critiques très violentes de Jean-Yves Girard à l'égard d'Herbert Simon, qui avait fait « retrouver » les lois de Kepler à son ordinateur, à partir des données expérimentales. Pour Girard, c'est inepte et relève d'une conception extrêmement naïve de la démarche scientifique, car la difficulté était d'imaginer la présence de la relation en question dans les données, plus que de la dégager de ces dernières, surtout pour un astrologue comme Kepler. Il remarque également qu'il aurait été intéressant de savoir si l'ordinateur a retrouvé la quatrième « loi » de Kepler, qui était fausse.
Un article qui discute de la Goëdelite et du « Simonisme ».
@A. oui mais justement je trouve que les scientifiques interrogés dans l'article de la bbc sont plutôt conscients des limites de leur approche. Ils signalent bien que ce robot joue le rôle d'un junior lab assistant et pas d'un scientifque humain. Ce qui est normal, il ne fait que produire des données brutes en appliquant des procédures standardisées qui doivent s'appuyer sur les « vraies » théories développées en génétique.
De plus ils signalent avec amusement qu'au prix qu'à coûté le robot, des humains seraient arrivés au même résultat.
L'un des problèmes, c'est que c'est une mise en avant de l'approche génétique (résumée dans ce passage :
"It's like a car," Professor King said. "If you remove one component from the engine, then drive the car to see how it performs, you can find out what that particular component does."
) au moment même où on se rend compte des limites de cette même approche. Cela laisse penser que la biologie, c'est l'approche génétique : c'était vrai et important ces 50 dernières années, mais cela doit changer. Cela va aussi dans la droite ligne de ce qu'on appelle dans le jargon le "high-troughput data" qui est très à la mode mais est à mon avis une approche très conservative et peu créative, là où on a certainement besoin de nouvelles approches pour progresser (en particulier des approches qui voient plus le vivant comme un système dynamique).
Enregistrer un commentaire