Résultats liés à « Informatique »

Intelligence artificielle et auto-apprentissage

Physical Review Letters

L’équipe « Reservoir Computing » – OPERA-Photonique dirigée par Marc Haelterman et le Laboratoire d’Information Quantique dirigé par Serge Massar – viennent de réaliser un calculateur analogique photonique inspiré du fonctionnement du cerveau et des dernières avancées en intelligence artificielle. La principale innovation de leur dispositif expérimental est qu’il peut être utilisé tant pour réaliser des tâches de calcul comme la reconnaissance de la parole, que pour améliorer ses propres performances (Physical Review Letters, 16 sept 2016). Pour en savoir plus sur ce projet

IBM Faculty Award décerné au Pr. Jean-François Raskin

 jfraskinL’IBM Faculty award 2014 a été décerné au Pr. Jean-François Raskin pour ses contributions essentielles à la recherche sur la vérification assistée par ordinateurs. Le Pr. Jean-François Raskin développe en effet de nouveaux modèles mathématiques quantitatifs et hybrides pour les systèmes informatiques embarqués. Pour en savoir plus sur son projet

Les preuves mathématiques pour assurer la correction des systèmes informatiques embarqués et d’intelligence artificielle
Jean-François Raskin

Développement de nouveaux modèles mathématiques quantitatifs et hybrides pour les systèmes informatiques embarqués, d’intelligence artificielle et l’analyse de la dynamique des systèmes biologiques.

Dernières nouvelles:

  • L’équipe du Pr. Raskin est partenaire du projet « Verifying Learning Artificial Intelligence Systems » du programme interuniversitaire Excellence of Science 2017-2021 avec des   équipes de la KULeuven et de l’Université de Namur.
  • Le Pr. Jean-François Raskin est élu par ses pairs dans le « working group 2.2 » de l’International Federation for Information Processing.
  • L’équipe du Pr. Jean-François Raskin remporte une Action de Recherche Concertée Advanced 2016-2021
  • Pr. Jean-François Raskin reçoit un mandat de Professeur Francqui pour les années 2015-2018
  • Pr. Jean-François Raskin is awarded with the 2014 IBM Faculty Award
  • Pr. Jean-François Raskin is awarded with the 2014 the silver medal of the Kurt Gödel Society for his prototype of  automatic synthetis

Biographie

Né en 1972. Docteur en Sciences des Facultés Universitaires Notre-Dame de la Paix (Namur), Post-doctorat à UC Berkeley et au Max-Planck Institute de Saarbrücken. Professeur et ancien Président du Département d’Informatique de la Faculté des Sciences de l’ULB. Il a été notamment Professeur invité à l’Ecole Polytechnique Fédérale de Lausanne et à L’Ecole Normale Supérieure de Cachan.

Cliquez ici pour lire davantage à ce propos

Projet

1. APPLICATIONS COMPLEXES ET LOGICIELS CORRECTS

Screen Shot 2013-12-05 at 18.06.04

Aujourd’hui, de nombreuses applications complexes et critiques, telles que l’assistance au pilotage d’un avion ou la régulation du rythme cardiaque par un pacemaker, sont mises en œuvre à l’aide de programmes informatiques.

Pour ces applications critiques, il est primordial de s’assurer que le logiciel construit est correct.

Ecrire un logiciel correct est une tâche difficile. Un logiciel peut en effet comporter plusieurs centaines de milliers de lignes de code et une seule erreur dans un programme peut avoir des conséquences désastreuses.

Malheureusement,  il est encore plus difficile de prouver (mathématiquement) qu’un logiciel ne contient aucune erreur.  Aussi, des recherches sont menées pour concevoir des algorithmes, et donc des programmes informatiques, capables de construire des preuves de correction.

Notre projet de recherche se situe précisément dans le domaine fascinant de la « vérification assistée par ordinateur » (V.A.O). Dans ce cadre, nous développons de nouveaux modèles mathématiques et l’algorithmique nécessaire à leur analyse automatique.

2. AU-DELA DU MODELE BOOLEEN : EXTENSIONS QUANTITATIVES ET MODELES HYBRIDES

Screen Shot 2013-12-05 at 18.06.13Les modèles et les notions de corrections développés jusqu’à présent dans le domaine de la vérification assistée par ordinateur peuvent être qualifiés de « Booléens ». En effet, ils permettent d’établir qu’un programme est correct ou non. Ils ne permettent pas d’établir des critères de qualité plus fins.

Par exemple, un logiciel pour pacemaker doit opérer des choix en « temps réel » en fonction du comportement du cœur du patient. Si des arythmies sont détectées, le logiciel commande l’émission et l’intensité d’impulsions électriques qui auront pour effet de rétablir un rythme cardiaque plus adéquat.

La correction du logiciel qui pilote les impulsions électriques est donc primordiale. Au surplus, il faut trouver une solution qui soit la plus parcimonieuse possible. En effet, afin de garantir une qualité de vie optimale au patient, le pacemaker ne doit intervenir que si cela est nécessaire.

Pour modéliser cette notion d’optimalité, nous avons donc besoin de modèles mathématiques plus riches qui permettent de modéliser des quantités (comme la fréquence des interventions du pacemaker) et de raisonner sur ces dernières.

3.LE PROJET :  DEFINIR UNE THEORIE SOLIDE POUR DEVELOPPER DE NOUVEAUX OUTILS POUR LA VERIFICATION DE SYSTEMES COMPLEXES

Screen Shot 2013-12-05 at 18.06.25Pour développer ces nouveaux outils informatiques, nous avons besoin de faire des progrès dans notre compréhension des propriétés fondamentales des nouveaux modèles mathématiques envisagés et de leurs algorithmes d’analyse.

Théorie des automates et les logiques associées

La théorie des automates finis est un des socles fondamentaux sur lesquels reposent les algorithmes de vérification de propriétés de correction des logiciels embarqués.

Depuis quelques années, des travaux de recherche visent à étendre ces théories avec des aspects quantitatifs : soit en ajoutant des variables à valeurs numériques aux automates finis pour contrôler plus finement leur exécution, soit en considérant les automates non plus comme définissant une fonction Booléenne mais une fonction dont la valeur est prise dans un domaine  infini, comme les réels ou les rationnels par exemple.

Ces modèles de calcul plus riches permettent la modélisation de systèmes informatiques plus complexes.

Pourtant, de nombreuses questions fondamentales sur ces formalismes restent ouvertes : quelle est l’expressivité des différentes classes d’automates? quelles sont les logiques équivalentes aux automates?  quelles nouvelles notions de corrections peuvent être formalisées? ces formalismes sont-ils robustes ?

Algorithmes ou semi-algorithmes pour les modèles quantitatifs.

Les problèmes de vérification que nous devons considérer sur les modèles quantitatifs sont généralement plus complexes que pour les modèles classiques, d’un point de vue conceptuel mais également d’un point de vue calculatoire.

Plusieurs problèmes importants (comme le problème d’inclusion de langages) ont déjà été montrés indécidables pour les extensions quantitatives. D’autres problèmes restent décidables mais le coût de leur résolution est très nettement accru.

Néanmoins, pour les problèmes indécidables, il convient de comprendre la frontière de décidabilité et également de proposer des solutions approchées -basées par exemple sur l’interprétation abstraite- ou encore des semi-algorithmes symboliques afin d’obtenir des solutions qui ont un intérêt dans la pratique.

Pour obtenir des résultats significatifs dans ce domaine, nous avons donc besoin de faire des avancées majeures dans notre compréhension des problèmes situés à la frontière de l’informatique théorique et des mathématiques. Ces avancées seront la base de nouveaux outils informatiques d’analyse de systèmes complexes.

Les systèmes « hybrides »

Un système informatique embarqué est typiquement un système « hybride » puisqu’il vise à contrôler un processus physique -dont l’évolution est continue- par l’intermédiaire de décisions discrètes qui auront en retour un effet sur l’évolution continue du système.

Les systèmes biologiques sont également des systèmes de nature hybride. En effet, la concentration d’une protéine évolue de façon continue dans le temps alors que l’activation ou l’inhibition d’un gène résultant dans le changement de mode de fonctionnement biochimique d’une cellule est typiquement un événement discret.

Ce dernier point est important pour comprendre l’une des applications que nous visons.

4. APPLICATIONS VISEES : systèmes embarqués  et  modélisation des systèmes biologiques

VERS LA CERTIFICATION DES SYSTEMES EMBARQUES

Les systèmes informatiques embarqués sont une cible privilégiée pour ces nouveaux modèles mathématiques. Les nouveaux outils de vérification que nous développerons permettront une conception plus rigoureuse de ces systèmes informatiques embarqués. Ils permettront également de certifier leur correction à l’aide de preuves mathématiques.

Il y a actuellement une demande importante pour des avancées en vérification assistée par ordinateur dans des domaines aussi importants que l’informatique pour les applications spatiales, l’aéronautique, les équipements médicaux, les microprocesseurs, la sécurité nucléaire, etc.

MACHINE LEARNING ET SYSTEMES D’INTELLIGENCE ARTIFICIELLE

Recently, artificial intelligence (AI) has made substantial progresses in a series of applications domains: driverless cars, IBM’s Watson program, deep learning techniques for playing Go, are popular examples. But those recent AI’s progresses also trigger important new questions about the future: what AI systems will be able to do, what they should be allowed to do, and what the implications are for humans.

The ongoing debate has motivated the AI and computer science communities to investigate what constitutes “safe AI” and whether it is possible to develop such “safe AI” systems that can be trusted. Quoting Dr. Guruduth Banavar, Vice President of IBM Research: ”Artificial intelligence is not without its risks. But we believe the risks are manageable. And that the far greater risk would be to stifle or otherwise inhibit the development of a technology with the potential to greatly improve the quality of life around the world. […] To reap the societal benefits of AI systems, we will first need to trust it. […] Trust is built upon accountability. As such, the algorithms that underpin AI systems need to be as transparent, or at least interpretable, as possible.” In this project, we want to push this research agenda and we claim that AI systems must also be mathematically verifiable. The trust in system is particularly important for systems that are safety critical (this is the case for example for driverless cars).

Our project aims at providing theoretical foundations and algorithmic methods to support the design of safer artificial intelligence systems that use learning. Tackling this important, timely and ambitious research agenda, requires on the one hand, extending verification models, and design methodologies, and verification algorithms to cover AI systems that learn, and on the other hand, improving learning methods so that they provide guarantees that can be used in verification.

As a starting point for our research, we will build on mathematical models and algorithms that we have developed in a recent project founded by European Research Council. In the context of this project, we have generalized transition systems and automata – models of computation in the classical approach to verification – by the more flexible, and mathematically deeper, game-theoretic and stochastic frameworks.

We intend to pursue this research work in collaboration with researchers active in the area of learning and articifical intelligence. To this aim, we have recently established a collaboration with a world renowed team at KULeuven.

MODELISATION DES SYSTEMES BIOLOGIQUES

Notre projet inclut également un pan novateur qui vise spécifiquement la recherche en biologie.

En effet, les modèles mathématiques hybrides que nous développons sont également bien adaptés à la modélisation et l’analyse de la dynamique des systèmes biologiques.

Certes, les biologistes possèdent des outils performants pour la modélisation de leurs systèmes, mais ces outils sont basés principalement sur les équations différentielles, soit les mathématiques du continu.

Malgré une réelle demande provenant des biologistes pour des outils de modélisation hybrides, plus adaptés à la nature -même des systèmes qu’ils étudient, les avancées dans ce domaine sont encore timides : seulement une dizaine de laboratoires au monde travaillent sur cette question.

Pour progresser de manière significative dans ce domaine, nous collaborerons avec des collègues spécialisés en biologie théorique, notamment via l’engagement d’un post-doc formé à la modélisation des systèmes biologiques qui pourra nous fournir des études de cas réalistes sur lesquels nos nouveaux formalismes mathématiques pourront  être appliqués.

Notre recherche permettra donc de faire avancer la modélisation de la dynamique des systèmes biologiques en la rendant plus simple, plus efficace et en somme, plus proche de la réalité.

 

5. GROUPE DE METHODES FORMELLES et VERIFICATION ASSISTEE PAR ORDINATEUR (ULB)

Screen Shot 2013-12-05 at 18.06.34Le groupe « Méthodes Formelles et Vérification Assistée par Ordinateur » a été créé en 2000 au sein du Département d’Informatique de la Faculté des Sciences de l’ULB.

Le groupe est la référence belge dans le domaine de la vérification assistée par ordinateur (V.A.O.) et de nombreux chercheurs étrangers visitent régulièrement Bruxelles pour collaborer avec le groupe du Prof. Jean-François  Raskin.

Le groupe coordonne par ailleurs le Centre Fédéré en Vérification  du FNRS qui rassemble toutes les équipes universitaires belges actives dans le domaine de la V.A.O.

Le groupe est également très actif dans le concert de la recherche européenne et a participé  (comme membre ou coordinateur)  à plusieurs projets de recherche européens d’envergure : FP7 NoE, FP7 STREP, ESF Eurocores, ESF Networks, COST Actions, etc.

Dans les prochains mois, le groupe du Pr. Raskin participera également à un nouveau projet de recherche européen, financé par l’action Future and Emerging Technologies du 7e Programme Cadre qui visera à mettre au point de nouveaux outils de développement de systèmes informatiques complexes à l’aide de la théorie des jeux.

Le groupe a une expertise reconnue dans les thématiques suivantes: systèmes hybrides et temps-réels, systèmes à espaces d’états infinis, model checking, algorithmes symboliques basés sur les antichaînes, algorithmes de synthèse basés sur la théorie des jeux.

Budget sur 4 ans

RESSOURCES HUMAINES

Deux chercheurs post-doctorants avec une expérience de recherche en informatique théorique travailleront sur les fondations mathématiques et algorithmiques.

Ils développeront également des outils de vérification pour les nouveaux formalismes.

Ces chercheurs collaboreront avec un biologiste ayant une expertise en modélisation des systèmes biologiques pour appliquer les théories et outils développés.

FONCTIONNEMENT ET EQUIPEMENTS

Afin de développer l’expertise en modélisation des systèmes biologiques, des échanges scientifiques de moyenne durée seront organisés chez des collègues étrangers spécialisés dans la modélisation de tels systèmes à l’aide d’automates (IST Austria, UPenn et UC Berkeley).

Par ailleurs, des ordinateurs performants seront nécessaires au développement des outils informatiques pour l’analyse de modèles mathématiques complexes. Ces équipements seront également utilisés pour l’analyse de modèles de systèmes embarqués et de systèmes biologiques.

L’analyse de ces modèles requiert des ressources de calcul importantes et dédiées.

Cliquez ici pour dérouler le tableau du budget

Autre

La fiche du projet disponible au format PDF ici.