Je vais présenter la construction de complétions de Rezk “strictes”. En théorie des types homotopique, la complétion de Rezk d'une catégorie C est une catégorie univalente équivalente à C. Dans un cadre plus spécifique (les ensembles cubiques), la complétion de Rezk stricte permet de plus de conserver certaines égalités strictes (lois d'associativité et de neutralité).

Cette construction s'applique non seulement aux catégories, mais aussi aux modèles de la théorie des types. Elle permet alors de prouver la canonicité homotopique pour la théorie des types homotopique. Plus de détails peuvent êtres trouvés dans https://arxiv.org/abs/2311.05849.

(Note that the talk will be in fench.) This talk presents a constructive approach to trigonometry, fully formalized and proven in the Coq proof assistant, that avoids the use of π. Angles are defined as pairs of reals. Along the way, some classical trigonometric formulas naturally emerge. The process culminates in the definition of dividing an angle by an integer, achieved through a convergent sequence. No prior knowledge of Coq is required to understand the talk, as no Coq code appears in the slides. While the talk is given in French, the slides are in English, allowing non-French speakers with a basic understanding of French to follow along.

Large Language Models (LLMs) have proved surprisingly effective at solving a wide range of tasks from just a handful of examples. However, their lack of reliability limits their capacity to tackle large problems that require many steps of reasoning. In response, researchers have proposed advanced pipelines that leverage domain-specific insights to chain smaller prompts, provide intermediate feedback and improve performance through search. However, the current complexity of writing, debugging, tuning and maintaining such pipelines has put a bound on their sophistication.

We propose a new paradigm for programming with LLMs called oracular programming. In this paradigm, domain experts are invited to define high-level problem-solving strategies as nondeterministic programs. Such programs are reified into infinite search trees for LLM oracles to navigate. A separate demonstration language allows annotating choice points with examples, while keeping them grounded and synchronized as the associated program evolves.

In this talk, I will motivate and explain the key concepts of oracular programming. I will introduce Delphyne, a framework for oracular programming based on Python, discuss the associated tooling, and demonstrate Delphyne on a program verification case study. Hopefully, such a framework can foster research on intersymbolic AI and facilitate creative combinations of LLMs with symbolic provers.