Florian Cassayre

Simon Guilloud, Florian Cassayre, Viktor Kunčak

We present the foundations and initial implementation of a new interactive theorem prover, named LISA. In a slight contrast to most popular type-theoretic frameworks, and much like Mizar, LISA aims to use classical mainstream foundations of mathematics, taking a hint, among others from the talk of John Harrison in this very venue in 2018. LISA uses (single-sorted) first order logic (with schematic variables) as the syntactic framework and set theory axiom schemas as the semantic framework. On top of these foundations we can construct numbers and other mathematical theories and models of computation without introducing new axioms. As the target use of LISA we envision mathematical statements as well as formal proofs of computer programs and systems, possibly with probabilistic and distributed behavior. For automation in LISA we expect to employ newly developed algorithms for equivalence checking of formulas and proofs, existing high-performance superposition-based theorem provers such as Vampire, SPASS, E and Zipperposition, as well as SMT solvers such as Z3, CVC5, and veriT, and OpenSMT. An important aim of LISA is interoperability with other proof assistants. We hope that the design of LISA with small, fresh code base, simple foundation and explicit proof objects will encourage building bridges with other tools. We also expect that the system will serve as a good vehicle to explore machine-learning guided superposition proof search, with learned heuristics complementing hand-tuned ones. We also plan to explore high-level translation of proofs from other systems into LISA, inspired by the success of deep neural networks in natural language translation.

Qiyuan Liang, Florian Cassayre, Haley Owsianko, Majed El Helou, Sabine Süsstrunk

Deep image denoisers achieve state-of-the-art results but with a hidden cost. As witnessed in recent literature, these deep networks are capable of overfitting their training distributions, causing inaccurate hallucinations to be added to the output and generalizing poorly to varying data. For better control and interpretability over a deep denoiser, we propose a novel framework exploiting a denoising network. We call it controllable confidence-based image denoising (CCID). In this framework, we exploit the outputs of a deep denoising network alongside an image convolved with a reliable filter. Such a filter can be a simple convolution kernel which does not risk adding hallucinated information. We propose to fuse the two components with a frequency-domain approach that takes into account the reliability of the deep network outputs. With our framework, the user can control the fusion of the two components in the frequency domain. We also provide a user-friendly map estimating spatially the confidence in the output that potentially contains network hallucination. Results show that our CCID not only provides more interpretability and control, but can even outperform both the quantitative performance of the deep denoiser and that of the reliable filter, especially when the test data diverge from the training data.

Florian Cassayre

Nous proposons un cadriciel pour le nouvel assistant de preuve LISA. Les deux systèmes sont basés sur le calcul des séquents de Gentzen en utilisant la logique du premier ordre, et sont implémentés dans le langage de programmation Scala. Notre système prend en charge différents styles de preuve et apporte un langage déclaratif pour les tactiques. L'utilisation des tactiques est facilitée par un système d'inférence des paramètres. Les preuves écrites dans ce cadre peuvent ensuite être traduites vers le noyau de confiance pour y être vérifiées. Nous montrons que notre cadre permet de simplifier le processus d'écriture de démonstrations formelles pour LISA, et qu'il est adapté à une utilisation interactive. Nous présentons d'autres composantes clés pour LISA, telles qu'une interface de programmation fortement typée, un analyseur syntactique ainsi qu'un système d'impression élégante, et un simplificateur de preuves.

Thèse de Master à LARA (Lab for Automated Reasoning and Analysis), EPFL.

Florian Cassayre

The goal of this semester project was to design a proof framework and use it to formalize elementary set theory. Safety is ensured by the compiler through type checking, while formal soundness is guaranteed by the execution. This hybrid verification process allows the framework to be used interactively inside an IDE. It is shown how types can encode logic formulas, in particular first order logic and higher order theories.

Projet de semestre réalisé à LARA (Lab for Automated Reasoning and Analysis), EPFL.