Rencontre, 22 septembre 2022
Programme
- 10:30 – 12:00
-
Romain Couillet (Université Grenoble-Alpes)Invited talk: Pourquoi et comment démanteler l'IA et le numérique?
(the talk will be given in french)
La civilisation occidentale est engagée depuis 10,000 ans dans un processus technicien, aujourd'hui verrouillé par une ontologie naturaliste (cette vision du monde qui fait de la "nature" le grand supermarché de l'humanité) qui entraîne dans son sillon les dynamiques exponentielles des consumérisme, extractivisme et colonialisme. La conséquence immédiate en est la destruction des écosystèmes (6e extinction de masse, 30x plus rapide que l'extinction du Crétacé et s'accélérant) et le dérèglement des dynamiques géophysiques planétaires (réchauffement, déplétions minérales). De gré ou de force (pic pétrolier, pénuries de ressources, chocs environnementaux et alimentaires), la société occidentale telle que nous la connaissons s'effondrera, vraisemblablement au cours de notre génération. Les technologies numériques, dont le point d'orgue est l'intelligence artificielle (IA), contribuent tout à la fois à la destruction socio-environnementale mais surtout à la perte massive d'outils de résilience (interpénétration de tous les domaines techniques, dépendance au pétrole, dépendance aux machines, dépendance aux décisions automatiques) en vue de la transition post-industrielle (retour à la terre et à l'artisanat), comme l'illustre parfaitement le cas de Cuba en 1990.
Dans cette présentation, je ferai un état des lieux de la situation du numérique et de l'IA, vus par Alexandre Monnin comme des technologies "zombie" (vivantes aujourd'hui mais de fait déjà mortes), et questionnerai les pistes de leur démantèlement nécessaire, de mon point de vue un axe prioritaire de la recherche numérique aujourd'hui. J'évoquerai ensuite la question anthropologique de l'ontologie naturaliste occidentale, absolument unique dans l'histoire de l'humanité, et en conflit avec les connaissances ethnographiques, de psychologie sociale et cognitive modernes: en deux mots, nous n'avons pas besoin d'un nouveau récit pour le monde, mais de retisser les liens animistes avec le vivant qui sont une partie intégrante de notre ADN, aujourd'hui masquée par notre culture et nos tabous auto-destructeurs. Ce travail écopsychologique est, selon moi, la clé de voûte de l'engagement de tou·tes les chercheur·ses-ingénieur·es vers la transition nécessaire, enthousiaste, collective et interspécifique que nous devons mener.
- 14:00 – 15:00
-
Guillaume Geoffroy (IRIF)Invited talk: A first-order completeness result about characteristic Boolean algebras in classical realizability
We prove the following completeness result about classical realizability: given any Boolean algebra with at least two elements, there exists a Krivine-style classical realizability model whose characteristic Boolean algebra is elementarily equivalent to it. This is done by controlling precisely which combinations of so-called “angelic” (or “may”) and “demonic” (or “must”) nondeterminism exist in the underlying model of computation.
- 15:00 – 16:00
-
Claudia Faggian (CNRS - IRIF)
(joint work with Thomas Ehrhard and Michele Pagani )
This talk proposes a proof-theoretical account of Bayesian Inference, by uncovering a close correspondence between two graphical languages, namely Bayesian Networks and Proof Nets. The former is a prominent graphical model for probabilistic reasoning. The latter is a graph formalism for Linear Logic proofs and (via the Curry-Howard correspondence of proofs as programs) a powerful tool to analyze the dynamics of proof/the execution of programs. Their natural interpretation into Probabilistic Coherence Spaces makes Proof Nets into probabilistic models.
The correspondence which we develop involves both the representation and the computation of a probabilistic model. In particular, we relate the most widely used algorithm for exact inference (message passing over clique trees) with the inductive interpretation of a proof, opportunely factorized into a composition of smaller proofs. The correspondence turns out to be so tight, that even the computational cost of inference is similar. We will also discuss some of the perspectives which proof theory could bring, such as compositionality (via types) and structure (hierarchical models).
