Artwork

Contenu fourni par Yann LeCun. Tout le contenu du podcast, y compris les épisodes, les graphiques et les descriptions de podcast, est téléchargé et fourni directement par Yann LeCun ou son partenaire de plateforme de podcast. Si vous pensez que quelqu'un utilise votre œuvre protégée sans votre autorisation, vous pouvez suivre le processus décrit ici https://fr.player.fm/legal.
Player FM - Application Podcast
Mettez-vous hors ligne avec l'application Player FM !

Leçon inaugurale : L'apprentissage profond : une révolution en intelligence artificielle - VIDEO

1:30:16
 
Partager
 

Série archivée ("Flux inactif" status)

When? This feed was archived on September 06, 2020 22:08 (3+ y ago). Last successful fetch was on April 07, 2020 16:50 (4y ago)

Why? Flux inactif status. Nos serveurs ont été incapables de récupérer un flux de podcast valide pour une période prolongée.

What now? You might be able to find a more up-to-date version using the search function. This series will no longer be checked for updates. If you believe this to be in error, please check if the publisher's feed link below is valid and contact support to request the feed be restored or if you have any other concerns about this.

Manage episode 187910522 series 1564458
Contenu fourni par Yann LeCun. Tout le contenu du podcast, y compris les épisodes, les graphiques et les descriptions de podcast, est téléchargé et fourni directement par Yann LeCun ou son partenaire de plateforme de podcast. Si vous pensez que quelqu'un utilise votre œuvre protégée sans votre autorisation, vous pouvez suivre le processus décrit ici https://fr.player.fm/legal.
Yann LeCun Informatique et sciences numériques Chaire annuelle en partenariat avec l'Inria Année 2015-2016 L'apprentissage profond : une révolution en intelligence artificielle Leçon inaugurale Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen. Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015. Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.
  continue reading

18 episodes

Artwork
iconPartager
 

Série archivée ("Flux inactif" status)

When? This feed was archived on September 06, 2020 22:08 (3+ y ago). Last successful fetch was on April 07, 2020 16:50 (4y ago)

Why? Flux inactif status. Nos serveurs ont été incapables de récupérer un flux de podcast valide pour une période prolongée.

What now? You might be able to find a more up-to-date version using the search function. This series will no longer be checked for updates. If you believe this to be in error, please check if the publisher's feed link below is valid and contact support to request the feed be restored or if you have any other concerns about this.

Manage episode 187910522 series 1564458
Contenu fourni par Yann LeCun. Tout le contenu du podcast, y compris les épisodes, les graphiques et les descriptions de podcast, est téléchargé et fourni directement par Yann LeCun ou son partenaire de plateforme de podcast. Si vous pensez que quelqu'un utilise votre œuvre protégée sans votre autorisation, vous pouvez suivre le processus décrit ici https://fr.player.fm/legal.
Yann LeCun Informatique et sciences numériques Chaire annuelle en partenariat avec l'Inria Année 2015-2016 L'apprentissage profond : une révolution en intelligence artificielle Leçon inaugurale Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen. Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015. Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.
  continue reading

18 episodes

Tous les épisodes

×
 
Loading …

Bienvenue sur Lecteur FM!

Lecteur FM recherche sur Internet des podcasts de haute qualité que vous pourrez apprécier dès maintenant. C'est la meilleure application de podcast et fonctionne sur Android, iPhone et le Web. Inscrivez-vous pour synchroniser les abonnements sur tous les appareils.

 

Guide de référence rapide