Thèse Dispatching et Reconstruction de Preuves Smt Via des Encodages Réutilisables dans le -Calcul Modulo Réécriture H/F - 75

Établissement : Université Paris-Saclay GS Informatique et sciences du numérique
École doctorale : Sciences et Technologies de l'Information et de la Communication
Laboratoire de recherche : Laboratoire Méthodes Formelles
Direction de la thèse : Frédéric BLANQUI ORCID 0000000174385554
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-03-22T23:59:59

Les solveurs SMT [BTB+24] sont largement utilisés pour vérifier la satisfaisabilité de formules logiques modulo des théories décidables (par exemple, l'arithmétique linéaire, les mots binaires). Étant donné qu'il s'agit de logiciels optimisés, complexes et volumineux, leurs résultats ne sont pas entièrement fiables. Pour renforcer notre confiance, ils produisent des preuves dans un format similaire à celui d'Alethe [SFBF21]. Cependant, ces preuves sont des preuves à grands pas: chaque étape peut constituer un raisonnement non trivial nécessitant de nombreux calculs et, parfois même, des recherches. Une solution pour garantir une confiance totale dans les preuves SMT serait de prouver la correction du code SMT lui-même, ce qui est impossible à réaliser et devrait de toute façon être répété à chaque modification du code. Une autre approche, plus simple et plus supportable, consiste à raffiner ces preuves à grands pas en étapes de preuve suffisamment petites dans un système logique bien défini, dont l'implémentation est suffisamment petite pour être certifiée, à l'instar des assistants à la preuve HOL-Light, Isabelle, Lean, Rocq, etc. Cependant, la traduction des problèmes vers les solveurs SMT et la reconstruction de leurs preuves nécessitent des encodages spécifiques à chaque assistant. Ceci engendre une duplication des efforts entre les systèmes et limite considérablement l'interopérabilité entre les solveurs SMT et les assistants de preuve. Une solution pour mutualiser ces efforts consiste à utiliser un cadre logique, c'est-à-dire un langage formel capable d'exprimer de manière unifiée les règles de déduction et les preuves de différents systèmes de preuve {HHP93]. Par exemple, les preuves de plusieurs démonstrateurs de théorèmes automatiques, solveurs SMT et assistants de preuve peuvent, dans une certaine mesure, être traduites vers le cadre logique Dedukti, ou son extension Lambdapi, et inversement, les preuves exprimées en Dedukti ou Lambdapi peuvent être retraduites vers plusieurs assistants de preuve [BDG+23]. Ce projet de thèse vise à développer, dans le cadre logique Lambdapi, un ensemble de bibliothèques et d'outils permettant d'extraire les composants communs au traitement des preuves SMT. L'objectif est de permettre aux assistants de preuve disposant d'une interface Lambdapi existante de réutiliser un pipeline commun pour la traduction des problèmes SMT et la reconstruction des preuves, réduisant ainsi le besoin d'encodages spécifiques à chaque assistant. De plus, nous visons à étendre les travaux existants sur la traduction des preuves Alethe vers Lambdapi en supportant davantage de théories (par exemple, les mots binaires, les tableaux et les chaînes de caractères).

This PhD project is about the certification of proofs generated by SMT solvers and their integration in proof assistants. SMT solvers and proofs assistants are theorem proving tools used in the formalization of mathematical proofs and in the verification of programs, protocols, etc. in the industry.

This PhD proposal aims at developing in the Lambdapi logical framework proof libraries and tools to factor out common proof-theoretic components of SMT reasoning. The goal is to enable proof assistants with an existing Lambdapi interface to reuse a common pipeline for SMT problem dispatching and proof reconstruction, reducing the need for repeated assistant-specific encodings. In addition, we aim at extending the existing work on the translation of Alethe proofs to Lambdapi [CDM24,CM25] by supporting more theories (e.g. bit vectors, arrays and strings).

SMT solvers are usually based on first-order logic or some slight extensions of it, while many proof assistants are based on more expressive logics like simple type theory (e.g. HOL-Light, HOL4, Isabelle) or dependent type theory (e.g. Agda, Lean, Rocq). Hence, if a proof assistant wants to use an external SMT solver to prove a formula F, it first has to transform F into a formula F\_smt, where every thing that is not part of the SMT logic has been 3abstracted away in such a way that one can build a proof of F from a proof of F\_smt.

Proof assistants currently work as follows: A translates F to F\_smt, sends F\_smt to a SMT solver, gets back a big-step proof, searches again for a proof of F but this time with its own tactics, using the SMT proof as a hint (hammer approach) [BKPU16], or by translating the SMT proof to A and deducing a proof of F from it (SMTCoq approach) [EMT+ 17]. In both cases, the first step (translation of F to F\_smt) and the last step (proof of F from proof of F\_smt) use codes and proof libraries specific to each proof assistant.

We propose a different approach aiming at making these two steps system-independent by leveraging the fact that we can have full and faithful mappings of the definitions and proofs of various proof assistants to Lambdapi. This approach consists in doing the first and last steps inside Lambdapi so that they can be exported to a new proof assistant as soon as a new mapping to Lambdapi is developed for this proof assistant. To do so, we will have to develop in Lambdapi a number of libraries and tools to transform F to F\_smt, obtain a proof of F from a proof of F\_smt, and handle new SMT theories (e.g. bit vectors, arrays, strings).