L'inria, au grand dam de nombre de ses salariés, a pactisé avec l'ennemi pour créer un laboratoire commun de recherche.
Pour le moment, les Forces du Mal ne semblent pas avoir imposé leur maléfiques brevets logiciels, et permettent même de libérer les sources et informations sur leur projet par une licence agréée par le Camp du Bien.
On y trouve divers axes de recherches très intéressants :
Secure Distributed Computations and their Proofs et Tools and Methodologies for Formal Specifications and for Proofs
En gros il s'agit de deux choses : de la cryptographie et de la vérification semi automatique de respect de séquence de protocoles en fonction de la spécification.
A ce propos, le gourou iMil, de la secte GCU, signalait l'autre jour un merveilleux logiciel, propre qui plus est, permettant d'implémenter des automates à état fini dans divers langages.
Un compilateur de machine à état fini, ça s'appelle Ragel et c'est génial ce truc !
Mathematical Components
L'idée est pas bête du tout : plutôt que de travailler à faire des outils de preuve de programme à approche globale, on cherche ici à prouver des petits bouts de code, de théorème afin de faciliter la preuve d'ensemble.
Ce travail de fourmi, utilisant le logiciel français COQ (développé à l'INRIA par des partisans résolus des Forces Du Bien), permettra d'étendre le domaine des logiciels prouvé formellement, qui sont encore peu nombreux (là où il y a risque pour la vie humaine).
On pourra noter des travaux précédents, comme why de Jean-Christophe Filliâtre.
Tools and Methodologies for Formal Specifications and for Proofs
On y utilise pour se faire les TLA, (Temporal logic of actions) de Leslie Lamport, qui lui aussi travaille pour les Forces du Mal, le but étant de construire un ensemble d'outil pour faire de la preuve logiciel avec.
Malgré tout, je comprend pas très bien pourquoi on essaye de combiner de la preuve pas model checker et de la preuve formelle, l'un est potentiellement le sous ensemble de l'autre, non ?
Dynamic Dictionary of Mathematical Functions
Encore d'après ce que j'ai compris, il s'agit de proposer une bibliothèque de d'équation typiques avec leur résolution (un peu comme si on donnait ax²+bx +c avec la méthode pour résoudre l'équation), le but étant de pouvoir rendre tout cela dynamique.
Ca aidera probablement nos amis du Cern à nous fabriquer un bau trou noir ;-)
Adaptive Combinatorial Search for e-Sciences
L'objectif est de fabriquer des solveur de problèmes complexes (recherche d'ensemble solution avec fonction solution à beaucoup beaucoup de variable je suppose) à partir de la programmation par contrainte. Les langages à programmation par contraintes sont lents, c'est connu.
ReActivity
En gros, c'est la digne suite des travaux de Douglas Engelbart (le type qui a inventé la souris avec son équipe) : comment rendre plus productif un scientifique avec des outils informatiques. On va plus loin que notre ami Douglas, car l'outil devient intelligent.
Un énorme potentiel là dedans, à suivre...
En passant... Qui sait qui va récupérer les brevets ? C'est...
Scientific Image and Video Data Mining
En gros, encore une fois d'après ce que j'ai compris, il 's'agit de détecter des pattern "complexes" dans de la vidéo et de l'image. Complexe signifie plus seulement reconnaitre des formes, mais des raisonnement analytiques applicables sur ces images.
J'adore le texte d'introduction qui nous raconte que les gennnntils krosoft vont gentilment utiliser tout cela pour des choses aussi utiles que de la sociologie, de l'archéologie, toussa.
Bref de la bonne conscience en barre.
Bon, on remarque quand même qu'ils ont pas pu s'empêcher de lâcher "studies of consumer trends in commercials", histoire d'évoquer les choses véritablement sérieuses.
Ca a du leur échappé, c'était plus fort qu'eux...
Bref intéressant tout ça...
Moi ce que je vois, c'est que l'Inria est encore dirigé par des fonctionnaires avec une vision économique attardée de 20 ans (je dis ça, parce que j'en ai pratiqué quelque uns...), et la seul chose qu'ils sont capable de faire, c'est de vendre leur âmes à des grosse boites. Créer des startup en se disant que certaines pourront devenir de très gros business, mais vous n'y pensez pas, c'est beaucoup trop risqué !! Et ma carrière ?
Oui parce qu'en fait, quand les chargés de transfert industriels arrivent en poste, ils sont fonctionnaire stagiaire, eu égard aux statuts fossilisés de la fonction publique... Et il doivent prouver leur compétence en passant un contrat avec une grosse boite, voyez ?
(bon, je suis mauvaise langue, il ont fait http://www.inria-transfert.fr/fr/index.php , mais c'est à la franchouillarde, c'est pas la californie...)
Voilà, j'ai fait attention à pas trop pomper le monde informatique pour celui-ci, mais c'était dommage de ne pas pouvoir continuer le très intéressant débat qui pointait...
Journal Le labo commun Inria-Microsoft
2
fév.
2009
# eh eh
Posté par BAud (site web personnel) . Évalué à 6.
Merci pour ton analyse, le lien était
http://www.lemondeinformatique.fr/actualites/lire-le-labo-co(...)
Repomper tel quel un article, c'est effectivement s'exposer à voir son journal disparaître, seuls les admins étant en mesure de supprimer les portions en cause (et c'est lourd), côté modo c'est "effacer et l'indiquer à son auteur" sans trop se poser de questions... (merci à celles et ceux qui nous ont prévenu, bon il se reconnaîtra :D).
Un point que je n'ai pas creusé, c'est si l'INRIA a réussi à obtenir une vraie licence libre telle que la CeCILL pour les travaux qui en résulteraient ?
[^] # Re: eh eh
Posté par vida18 . Évalué à 3.
# Notices of the AMS
Posté par patrick_g (site web personnel) . Évalué à 3.
Ce travail de fourmi, utilisant le logiciel français COQ
A noter un numéro extrêmement intéressant des Notices de l'American Mathematical Society consacré en décembre dernier aux preuves par ordinateur :
http://www.ams.org/notices/200811/index.html
Les articles sont tous bien foutus mais j'ai particulièrement apprécié celui intitulé "Formal Proof—Getting Started" qui évoque les divers logiciels de preuve.
"HOL Light" contre "Mizar" contre "ProofPower" contre "Isabelle" contre "Coq".
Et que le meilleur gagne !
# Combiner les techniques
Posté par Thomas Douillard . Évalué à 4.
Combiner des techniques généralistes a des techniques spécialisées au hasard ? Appliquer les techniques spécialisées quand c'est possible et les autres quand c'est nécessaire, les unes devant être à priori plus efficaces que les autres mais ne traitant qu'un sous ensemble de problème.
Ou d'autres approches si les problèmes sont les mêmes, faut voir les hybridations possibles.
# Troll spotted
Posté par Moogle . Évalué à 2.
[^] # Re: Troll spotted
Posté par Ontologia (site web personnel) . Évalué à 2.
Durant ces 5 ans, il devraient réussir une valorisation industriel, mais pas forcément avec des grosses boites. Le lancement réussi d'une start-up prometteuse pourrait aussi être valorisée.
Quand au côté fonctionnaire, je me rappelle qu'il était difficile de les avoir au téléphone après 17h...
Mais je suis surement mal tombé, j'ai aussi vu des gens très impliqués (d'ailleurs ceux qui n'était pas joignable après 17h étaient tout aussi impliqués)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 3.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Troll spotted
Posté par Ontologia (site web personnel) . Évalué à 6.
- Le CNRS/INRIA, etc... actuel où on fait du fondamentale sans chercher de valorisation industriel. On fait du théorique, on laisse les théoriciens déterminer ce sur quoi ils doivent travailler (ie pas le gouvernement comme actuellement), car se sont eux qui savent où aller, pas des politiciens.
- Une couche dans laquelle des chercheurs et des ingénieurs de recherches intéressés par des valorisation industrielles à moyen/ court terme (de 15 à 5 ans) côtoient les chercheurs "fondamentaux" dans leur labo, font des stages chez eux, et voient comment combiner différents résultats théorique pour des valorisation intéressantes.
Risque de conflit idéologique à cet étage...
- La troisième couche utilise les résultats de la précédente presques prêt à passer en phase industriel. Des communiquants, marketeux, des ingénieurs viennent aider à monter le projet pour créer une start-up ou en collaboration avec une grosse boite, ça dépend des investissement nécessaires.
Cette couche, avec les gains perçu (les entreprises appartiennent en majorité à l'état, mais fonctionne comme des boites de droit privé), les impôts générés, les emplois créé finance la recherche fondamentale et permet de donner les véritables moyens que nos chercheurs méritent et que le gouvernement ne veut pas leur donner
Un travail théorique répondant à des problèmatique purement théoriques n'a que faire de problématiques parasites de rentabilité, nous sommes bien d'accord. Néanmoins, des papiers étant publiés, d'autres peuvent le lire et en faire quelques chose.
Conclusion : la recherche de valorisation industriel ne doit pas être systématique, mais quand un travail de recherche peut déboucher sur un concept industrialisable à moyen terme, il ne faut pas à mon avis se mettre des oeillères idéologiques.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Troll spotted
Posté par Amine Mokhtari . Évalué à 1.
Tu la mettrais dans quelles couches, toi ? :-D
[^] # Re: Troll spotted
Posté par kikicnrv . Évalué à 2.
Ça coûte des ronds quand même toutes ces recherches, ceux qui investissent veulent un retour sur investissement.
Et même dans le cas où ça ne sera pas pour faire forcément plein de bénéfices, ça permet toujours de récupérer des fonds pour continuer les recherches.
[^] # Re: Troll spotted
Posté par Thomas Douillard . Évalué à 5.
* assez aléatoire,
* difficilement quantifiable, quand tu cherches tu sais pas forcément ou tu vas arriver, sinon ce serait pas la peine de chercher ... en général t'as un axe de recherche, mais à l'intérieur de cet axe ça peut partir dans tous les sens en fonction d'un tas de chose (guidé par les applications, par ton inspiration, ...)
* que le passage de la recherche aux applications, ben c'est pas vraiment un boulot de chercheur à part entière ( en gros ça prend un temps énorme, les chercheurs ont pas forcément les compétences nécessaires, ...)
En gros les trucs qui sont valorisés (et valorisable) on sait pas forcément à l'avance ce que ça sera. Genre on peut chercher un truc valorisable et ça va foirer, on peut chercher un truc très théorique qui va trouver des applications évidentes à plus ou moins long terme ...
Bref, effectivement il faut avoir de l'argent pour chercher c'est évident, mais il faut aussi accepter que ça peut ne pas avoir d'application ... ou au moins pas d'application évidente, et ça c'est dûr dans un système ou on cherche la rentabilité à tout prix.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 3.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Troll spotted
Posté par kikicnrv . Évalué à 4.
je ne défends pas le principe qui veut que la recherche n'ait qu'un but lucratif immédiat, je le constate. Car, comme tout investissement à notre époque, il semble improbable de voir un valeureux chevalier de la noble cause venir investir pour mois de 20% de bénéfice immédiat.
Je caricature un peu mais c'est ce que je crois constater à tous les niveaux d'investissement.
Le problème est que la recherche coûte des fortunes et que personne n'est prêt à "donner" son argent pour le bien de la cause (pas plus moi qu'un autre).
Je ne suis pas du tout dans le milieu de la recherche, ce que je dis ici, je ne le tiens que des discussions que j'ai pu avoir avec des amis chercheurs, mais ce qui est ressorti de ces discussions c'est que (si je ne dis pas de bêtises) :
- La recherche publique en France a du mal à trouver des partenaires dans le privé, donc niveau financement c'est tendu parce que DIANTRE ! qu'est ce qu'on paye beaucoup d'impôts dans ce pays, c'est dramatique.
- La recherche dans le privé, toujours en France, est à un niveau ridicule comparé aux États-unis.
- Le 1er point implique que les recherches en France n'amènent que peu de retour sur investissement.
- Il semblerait au contraire que les recherches des États-unis aboutissent régulière à un bénéfice élevé (en terme d'argent hein, on s'en fout de ce qu'on trouve)
Ça c'est ce que j'ai souvent pu entendre dire, voir lire dans diverses articles (ça fait quand même quelques années que je ne me suis pas penché sur la question) => est ce que je me trompe ? M'as t-on menti ?
Si je ne me trompe pas : comment font les États-unis ? Ils font de la recherche bas de gamme et nous on est les gentils qui faisons la bonne recherche gratos ?
Quelle est la solution ? Tout le monde il est gentil, tout le monde il est beau, on fait de la recherche qui coûte la peau des fesses, ça nous rapporte rien, mais c'est pour la bonne cause donc c'est pas grave ? Moi je veux bien (si si, vraiment) mais qui paye ? L'état ?
L'état ce sont les citoyens, tu sais les gens qui râlent tout le temps parce qu'ils payent trop d'impôts.
Ça ne me plaît pas ce système où on ne recherche que pour gagner de l'argent.
De la même manière que la politique générale et actuelles des entreprises qui visent à gagner vite tout de suite plutôt que de viser la pérénité ne me plaît pas.
Mais alors on fait quoi ? On dit qu'on n'est pas d'accord ? Moi je ne vois pas de solution (un truc pragmatique quoi, pas une solution qui part du postulat que les gens sont tous gentils/généreux/réfléchis) donc je dis juste ce qu'il me semble avoir constaté.
J'allais oublié :
Nul doute que le monde entier a sûrement beaucoup gagné avec la théorie de la relativité, les nombres complexes etc ... Mais je ne suis pas sur que ceux qui se sont investis dans ces recherches aient gagnés à la hauteur de leur découverte. Tant mieux qu'il ait existé des gens pour s'investir de la sorte il fut un temps mais ce n'est plus le cas.
Encore une chose sur l'importance de trouver des applications industrielles :
L'histoire de l'ampoule telle que je la connais => Thomas Edison n'a pas créée la première ampoule (c'était un Anglais je crois, ou un Russe, je sais plus) mais c'est lui qui en a récolté tous les lauriers, de nombreuses villes lui en ayant acheté pour l'éclairage public.
Ça rejoint ce que je disais plus haut sur la France : j'ai l'impression qu'on invente plein de bonnes choses, qu'on se défend bien par rapport aux États-unis, mais que eux font largement plus de bénéfices avec leurs recherches.
Pour conclure j'ai cru comprendre qu'avec la recherche sur le nucléaire (EPR, fusion tout ça) on a mis beaucoup de nos billes dans le même panier, mais là si on se démerde bien, il y a peut être de quoi gagner à long terme.
[^] # Re: Troll spotted
Posté par Nonolapéro . Évalué à 2.
La recherche fondamentale est indispensable parce qu'elle forme la base de nos connaissances, plus cette base sera large et solide plus on pourra aller loin.
[^] # Re: Troll spotted
Posté par ckyl . Évalué à 5.
Après ça n'empêche pas des collaboration avec d'autres boîtes. C'est à la discrétion de chaque équipe de recherche de choisir ses contrats.
Pour le cas du partenariat avec MS c'est encore autre chose. Les mecs de cambridge avaient envie de faire un tour à Paris. Pour être sérieux 5 minutes, Microsoft Research est un très gros acteur de la recherche fondamentale. Y'en a pas beaucoup qui hésiteraient entre un poste chez MS Research à cambridge, seattle ou Mountain View et un poste à l'INRIA. Bon c'est un tantinet plus difficile d'y rentrer mais c'est un détail...
Et autrement il y a quoi de plus sale de bosser avec MS Research, google labs, Yahoo Research et autres qu'avec des universités ?
# Tuning automatique de paramètres
Posté par Thomas Douillard . Évalué à 4.
L'objectif est de fabriquer des solveur de problèmes complexes (recherche d'ensemble solution avec fonction solution à beaucoup beaucoup de variable je suppose) à partir de la programmation par contrainte. Les langages à programmation par contraintes sont lents, c'est connu.
Juste un mot à ce propos. La programmation par contrainte, c'est une approche déclarative, en gros tu donnes des variables, exemple "entier a in [1..5], b in [10..12]]" et tu donnes des contraintes qui décrivent les solutions du problèmes (genre "a différent de b et a*a>2" ) dans un langage donné. Par exemple le sudoku peut se décrire par 81 variables dans [1..9] et quelques contraintes qui décrivent que les variables de la même ligne soient différentes, colonnes et les variables dans les carrés, soit un truc comme 27 contraintes du style "tous_différentes(A11,A12,...,A19) et ..."
Après le problème c'est pas tant que le langage soit lent qu'il soit plutôt générique et que tu peux décrire un paquet de problèmes différents, avec des caractéristiques différentes : beaucoup de solutions, pas de solutions, une seule solution, beaucoup ou peu variables par rapport aux contraintes, natures des contraintes, etc.
L'idée de la PPC c'est que tu décris ton problème et que tu laisse le solveur se débrouiller.
Malheureusement ça ne marche pas dans tous les cas et il faut parfois paramétrer le solveur dans le choix de ses algorithmes de résolution pour parvenir à une résolution efficace, ce qui nécessite un peu d'expertise dans le processus de résolution pour avoir une idée de ce qui peut marcher ou pas. Certain algo sont efficaces pour certaines forme de problème, dans d'autre cas ils sont trop couteux et ralentissent tout. Certaines heuristiques marchent uniquement dans certains cas, ...
L'idée ici c'est d'automatiser le tuning du solveur, le "adaptative" doit vouloir dire que ça doit se faire en cours de résolution. Genre le solveur teste un algo essaye de voir si ça a payé par rapport à autre chose, tente autre chose ... le tout idéalement sans faire intervenir l'utilisateur.
[^] # Re: Tuning automatique de paramètres
Posté par nojhan (site web personnel, Mastodon) . Évalué à 1.
Bref, le titre ne dit pas grand chose, en fait.
[^] # Re: Tuning automatique de paramètres
Posté par Thomas Douillard . Évalué à 2.
T'as même des gens qui font du continu et pas du combinatoire, de la satisfaction et pas de l'optimisation, en gros ouais ça a l'air assez fourre tout comme projet.
Du coup ça me fait penser qu'ils essayent de travailler dans les en:Hyper-heuristic ou qu'ils devraient jeter un oeil si pas déja fait.
( Çe truc c'est typiquement un truc de chercheur ;) )
[^] # Re: Tuning automatique de paramètres
Posté par scand1sk (site web personnel) . Évalué à 2.
[^] # Re: Tuning automatique de paramètres
Posté par Thomas Douillard . Évalué à 2.
Après t'as aussi ça : http://code.msdn.microsoft.com/solverfoundation un solver CSP et un solver LP (combinatoire) MILP et MINLP apparemment (mixte, linéaire et non linéaire et plus combinatoire pure pour le coup)
Sinon sur la page du projet t'as pas grand monde qui bosse sur SAT : http://www.msr-inria.inria.fr/Projects/adaptive-comb-search
Sinon j'ai pas compris ta phrase sur la combinatoire, tu veux dire que la combinatoire c'est la résolution systématique et autonome ou que ms fait de la résolution systématique et autonome sur SAT (problème combinatoire) ?
[^] # Re: Tuning automatique de paramètres
Posté par scand1sk (site web personnel) . Évalué à 1.
Je l'ai côtoyé essentiellement pour ses travaux sur SAT. Il y a des solveurs SAT en recherche locale et en recherche systématique effectivement, j'ai été un peu vite, mais ils sont tous autonomes. En programmation par contraintes, c'est loin d'être le cas, et la recherche systématique est à peu près… systématique.
[^] # Re: Tuning automatique de paramètres
Posté par Thomas Douillard . Évalué à 2.
[^] # Re: Tuning automatique de paramètres
Posté par Thomas Douillard . Évalué à 2.
# Scientific Image and Video Data Mining
Posté par regisb . Évalué à 3.
Je connais assez (très) bien les gens de l'INRIA impliqués dans ce projet, à savoir : Blake, Pérez, Ponce et Schmid. En fait : tout le monde (pas juste en France) dans ce domaine les connait parce qu'ils ont réalisé et continuent à réaliser des travaux de référence. Ce que je veux dire c'est que dans le domaine de la récupération d'images par le contenu, l'INRIA fait partie des institutions à la pointe de la recherche, en particulier pour ce qui concerne les applications des recherches.
Je ne m'étendrai pas sur l'activité de l'INRIA en général dans le domaine des logiciels libres, qui est forte. En particulier, je connais un paquet de chercheurs qui militent pour Scilab, une alternative libre à Matlab.
Par ailleurs, je ne ferai que mentionner les nombreux chercheurs qui sont encouragés par l'INRIA à dévouer 20% de leur temps à des activités professionnelles en dehors du cadre de la recherche. J'en connais, toujours dans le domaine du data mining, qui font du consulting dans des boîtes privées. L'incubateur de l'INRIA a également énormément de succès.
Enfin, le point le plus important : tout travail de recherche scientifique est destiné à être décrit et publié (encore une fois je ne parle que de ce que je sais, le data mining). Quand Microsoft fait de la recherche, ils publient. Dans les conférences de vision par ordinateur on retrouve tout un tas de gens de Microsoft Research qui réalisent des travaux très intéressants. Leurs méthodes sont systématiquement détaillées dans des articles disponibles et il n'est en général pas trop difficile pour un expert d'implémenter lui-même la méthode décrite.
La politique de Microsoft Research n'est pas la même que celle de Microsoft. En tant que chercheurs, ils ne cherchent pas le rendement à tout prix.
Je voulais donc démonter deux idées reçues que j'ai cru percevoir dans l'article :
1) L'INRIA serait un institut peu dynamique et peu compétitif alourdi par une hiérarchie statique.
2) L'INRIA vendrait son intelligence au service de Microsoft.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.