diff --git a/_data/seminar.yml b/_data/seminar.yml index 040d35dee399f9aecb91cb212a127928ee9d6540..3a6e971ba8a1ed3bbe38cd1514f8763e00c2156c 100644 --- a/_data/seminar.yml +++ b/_data/seminar.yml @@ -20,6 +20,19 @@ I present a method for computing statistically guaranteed confidence bands for functional surrogate modes: surrogate models which map between function spaces, motivated by the need build reliable physics emulators. The method constructs nested confidence sets on a low-dimensional representation (an SVD) of the surrogate model’s prediction error, and then maps these sets to the prediction space using set-propagation techniques. The result is conformal-like coverage guaranteed prediction sets for functional surrogate models. We use zonotopes as basis of the set construction, due to their well-studied set-propagation and verification properties. The method is model agnostic and can thus be applied to complex Sci-ML models, including Neural Operators, but also in simpler settings. An important step is a technique to capture the truncation error of the SVD, ensuring the guarantees of the method. A preprint is available here: [arXiv:arXiv.2501.18426](https://doi.org/10.48550/arXiv.2501.18426) +- date: 2025-03-24 14:00 + team: PARTOUT + room: Marcel-Paul Schützenberger + speaker: Niyousha Najmaei + picture: https://niyoushanajmaei.github.io/images/nioosha.png + website: https://niyoushanajmaei.github.io/ + lab: IRIF + title: A Type Theory for Comprehension Categories with Applications to Subtyping + abstract: | + We develop a type theory that we show is an internal language for comprehension categories. This type theory is closely related to Martin-Löf type theory (MLTT). Indeed, semantics of MLTT are often given in comprehension categories, albeit usually only in discrete or full ones. As we explain, requiring a comprehension category to be full or discrete can be understood as removing one “dimension” of morphisms. Thus, in our syntax, we recover this extra dimension. We show that this extra dimension can be used to encode subtyping in a natural way. Important instances of non-full comprehension categories include ones used for constructive or univalent intensional models of MLTT and directed type theory, and so our syntax is a more faithful internal language for these than is MLTT. + + Details can be found in the following preprint: +https://arxiv.org/abs/2503.10868 - date: 2025-03-17 14:00 team: PARTOUT room: Marcel-Paul Schützenberger