tag:blogger.com,1999:blog-2956815603489372083.post8018017590310236176..comments2024-03-24T13:57:07.411+01:00Comments on Anniceris: Les premiers Cylons chez les Assistants-ChercheursPhersvhttp://www.blogger.com/profile/10962408594713963134noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-2956815603489372083.post-7093555079922709602012-11-16T20:26:06.702+01:002012-11-16T20:26:06.702+01:00Ce commentaire a été supprimé par un administrateur du blog.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-53858892882625295012009-04-04T23:51:00.000+02:002009-04-04T23:51:00.000+02:00L'un des problèmes, c'est que c'est une mise en av...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 :<BR/><BR/><BR/>"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." <BR/><BR/><BR/>) 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).Tom Roudhttp://tomroud.comnoreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-46551470564635517762009-04-04T15:24:00.000+02:002009-04-04T15:24:00.000+02:00@A. oui mais justement je trouve que les scientifi...@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.<BR/>De plus ils signalent avec amusement qu'au prix qu'à coûté le robot, des humains seraient arrivés au même résultat.Duncanhttp://nanostelia.wordpress.comnoreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-50077875523065347032009-04-04T13:49:00.000+02:002009-04-04T13:49:00.000+02:00@Tom Roud: tout cela me rappelle les critiques trè...@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.<BR/><BR/>Un <A HREF="http://iml.univ-mrs.fr/~girard/godel.pdf.gz" REL="nofollow">article</A> qui discute de la Goëdelite et du « Simonisme ».A.https://www.blogger.com/profile/03954463506974679294noreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-90682101300321696102009-04-04T03:20:00.000+02:002009-04-04T03:20:00.000+02:00Dans le même numéro, il y a aussi un papier de l'é...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.<BR/>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 Roudhttp://tomroud.comnoreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-33239250484765557512009-04-04T00:25:00.000+02:002009-04-04T00:25:00.000+02:00@Phersv: à vrai dire, c'est déjà le cas dans au mo...@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.<BR/><BR/>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).<BR/><BR/>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.).<BR/><BR/>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.<BR/><BR/>La France a vraiment une grande expertise en la matière ; l'assistant de preuve <A HREF="http://coq.inria.fr" REL="nofollow">Coq</A> est une, sinon <B>la</B> référence en la matière.<BR/><BR/>Pour un revenir à la question initiale, la plateforme <A HREF="http://why.lri.fr" REL="nofollow">Why</A> 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é.A.https://www.blogger.com/profile/03954463506974679294noreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-5326607202644823682009-04-03T23:04:00.000+02:002009-04-03T23:04:00.000+02:00Merci, oui, 4, je corrige (et l'entrée dit que l'u...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).<BR/><BR/>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 ?Phersvhttps://www.blogger.com/profile/10962408594713963134noreply@blogger.comtag:blogger.com,1999:blog-2956815603489372083.post-57138247751721015402009-04-03T20:52:00.000+02:002009-04-03T20:52:00.000+02:00C'est le théorème des 4, et non 5, couleurs, qui a...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...Antonin & Damiahttps://www.blogger.com/profile/06209431779816050551noreply@blogger.com