00:00:00 / 00:00:00

Dependent Type Theory from the Perspective of Mathematics, Physics, and Artificial Intelligence

De David McAllester

Apparaît dans la collection : Mikefest : A conference in honor of Michael Douglas’ 60th birthday

Dependent type theory imposes a type system on Zemelo-Fraenkel set theory (ZFC). From a mathematics and physics perspective dependent type theory naturally generalizes the Bourbaki notion of structure and provides a universal notion of isomorphism and symmetry. This comes with a universal substitution theorem --- isomorphic objects are inter-substitutable in well-typed contexts (Hofmann and Streicher 1995). From an AI perspective, or automated reasoning perspective, dependent type theory underlies the LEAN interactive verifier which is currently the go-to system for formal verification of mathematics. This talk will review dependent type theory as a discipline on set theory (the set model of type theory) and discuss approaches to improving automated reasoning based on SMT (SAT Modulo a theory) technology. This results in a class of inference algorithms under the name SAT modulo type theory or SMTT. Speculations on the relationship between SMTT and deep learning will be discussed briefly.

Informations sur la vidéo

  • Date de captation 12/05/2022
  • Date de publication 13/05/2022
  • Institut IHES
  • Langue Anglais
  • Audience Researchers
  • Format MP4

Domaine(s)

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow




Inscrivez-vous

  • Mettez des vidéos en favori
  • Ajoutez des vidéos à regarder plus tard &
    conservez votre historique de consultation
  • Commentez avec la communauté
    scientifique
  • Recevez des notifications de mise à jour
    de vos sujets favoris
Donner son avis