~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:picube:index|Formath]]\\
Lundi 28 avril 2025, 14 heures, 3052 et en visio\\
**Rafaël Bocquet**  //Complétions de Rezk strictes//
<button type="link" size="xs" collapse="b32-4567">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b32-4567" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:picube:index|Formath]]\\
Lundi 10 mars 2025, 15 heures, 3052 (+visio)\\
**Daniel De Rauglaudre**  //Trigonometry Without π//
<button type="link" size="xs" collapse="b32-4568">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b32-4568" collapsed="true">
<well size="sm">
(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.
</well>
</collapse>


[[seminaires:picube:index|Formath]]\\
Lundi 10 février 2025, 14 heures, 3052\\
**Jonathan Laurent** (CMU) //Oracular Programming//
<button type="link" size="xs" collapse="b32-4569">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b32-4569" collapsed="true">
<well size="sm">
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.
</well>
</collapse>