Dissertationen zum Thema „Synthèse de preuves“

Présentation d'une approche déductive basée sur l'instantiation progressive de schémas de programmes fonctionnels. Un système formel de preuve est décrit dans lequel le lien entre schémas de programmes et schémas de propriétés est exhibe. La complétude relative et la correction de ce système sont prouvées notamment pour les fonctions partiellement définies. Des stratégies, guidées par l'utilisateur, sont ensuite proposées qui permettent de caractériser les propriétés nécessaires, propres à chaque schema, en termes de recherche de préconditions

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS
This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Cette thèse de doctorat est une investigation des logiques de la connaissance, de la croyance et de la dynamique d'information, en utilisant des outils de topologie et logique épistémique (dynamique). La partie I concerne les interprétations fondées sur des preuves de croyances justifiées et connaissance. Commencer par une interprétation topologique des connaissances désormais standard en tant qu'opérateur intérieur, nous développons, de manière progressive, un cadre qui (1) peut parler de preuves non seulement sémantiquement, mais aussi le niveau syntaxique, rendant ainsi la notion de preuve plus explicite; (2) prend la preuve comme la notion la plus primitive, et définit la croyance et la connaissance purement basé sur elle. Dans la partie II de cette dissertation, nous nous concentrons sur notions de connaissances ainsi que divers types de dynamique de l'information comprenant apprendre de nouvelles preuves. Plus précisément, cette partie est centrée autour des notions de certaines connaissances et savoir-faire en tant que «connaissances potentielles», ainsi que les liens entre la notion abstraite d'effort épistémique englobant toute méthode l'acquisition de preuves et les attitudes dynamiques bien étudiées telles que les annonces publiques arbitraires. Pour résumer, cette thèse réinterprète d'une part certaines logiques épistémiques et doxastiques existantes et leurs extensions dynamiques d'un point de vue topologique, fournissant une interprétation fondée sur des preuves. D'un autre côté, elle utilise des outils topologiques pour affiner et étendre les analyses antérieures, conduisant à de nouvelles logiques de la dynamique des preuves et de l'information
This dissertation brings together epistemic logic and topology. It studies formal representations of the notion of evidence and its link to justification, justified belief, knowledge, and evidence-based information dynamics, by using tools from topology and (dynamic) epistemic logic. Part I is concerned with evidence-based interpretations of justified belief and knowledge. Starting with a by-now-standard topological interpretation of knowledge as the interior operator, we develop, in a gradual manner, a topological framework that (1) can talk about evidence not only semantically, but also at the syntactic level, thereby making the notion of evidence more explicit; (2) takes evidence as the most primitive notion, and defines belief and knowledge purely based on it, thereby linking these two crucial notions of epistemology at a deeper, more basic level. In Part II of this dissertation, we focus on notions of knowledge as well as various types of information dynamics comprising learning new evidence. More precisely, this part is centered around the notions of absolutely certain knowledge and know ability as "potential knowledge", as well as the connections between the abstract notion of epistemic effort encompassing any method of evidence acquisition and the well-studied dynamic attitudes such as public and arbitrary public announcements. To sum up, this dissertation on one hand re-interprets some existing epistemic and doxastic logics and their dynamic extensions from a topological perspective, providing an evidence-based interpretation. On the other hand, it uses topological tools to refine and extend earlier analysis, leading to novel logics of evidence and information dynamics

L'activité physique (AP) est l'un des principaux programmes de soins de support recommandés par plusieurs directives pour améliorer les effets secondaires du cancer chez les survivants du cancer, à cause des preuves de son efficacité sur ces issues de santé. Cependant, les preuves de l'efficacité de l'AP sur le retour au travail (RAT) chez les survivants du cancer restent limitées et inconnues. De plus, on ne sait pas si les recommandations d’AP issues des directives existantes sont applicables au RAT après un diagnostic de cancer. L'objectif de cette thèse était d'évaluer les effets des programmes ou interventions d'AP sur le RAT chez les survivants du cancer et de fournir des preuves de l'efficacité de l'AP sur le RAT après un diagnostic de cancer. Pour répondre à la question de recherche, nous avons utilisé la méthodologie basée sur des preuves (revue systématique, méta-analyse et revue rapide). Cette thèse a montré que les programmes d’AP sont faisables et sans risque pour les patients atteints de cancer. Nous avons trouvé que les interventions d’AP ont des effets positifs significatifs sur le RAT chez les survivants du cancer. La dose d’AP comprise entre 7,6 et 15 METs.h/semaine, consistant en 100-120 minutes par semaine d’exercices aérobique et de résistance, d’intensité modéré à vigoureux, semblent être efficaces pour améliorer le RAT après cancer. En conclusion, cette thèse apporte des preuves modérées sur l’efficacité des interventions d'AP sur le RAT chez les survivants du cancer. Elle a également permis d’estimer la dose d’activité physique nécessaire pour améliorer le RAT chez les patients. À partir des résultats, nous avons proposé un guide avec des protocoles pratiques pour prescrire et implémenter des programmes d'AP pour soutenir la RAT chez les patients de cancer du sein
Physical activity (PA) is one of the leading supportive care programs recommended by several guidelines to improve most of cancer side effects experienced by cancer survivors, because of the strong evidence of its effectiveness on these health outcomes. However the evidence on the effectiveness of PA on return to work (RTW) in cancer survivors remains limited and unknown. In addition, it is unknown whether the recommendations from existing PA guidelines are applicable to RTW after cancer diagnosis. Therefore, the objective of this thesis was to evaluate the effects of PA programs or interventions on RTW in cancer survivors and provide evidence for the effectiveness of PA on RTW after a cancer diagnosis. To address the research question, we used evidence-based methodology (systematic review, meta-analysis, and rapid review). This thesis showed that PA programs are feasible and safe for cancer patients. We found that PA interventions have significant positive effects on RTW in cancer survivors. The dose of PA comprised between 7.6 and 15 METs.h/week, consisting of 100-120 minutes per week of moderate to vigorous intensity aerobic and resistance exercise, seem to be effective in improving RTW after cancer. In conclusion, this thesis provides moderate evidence on the effectiveness of PA interventions on RTW in cancer survivors. It also allowed us to estimate the dose of physical activity needed to improve RTW in cancer patients. Based on these findings, we proposed a guidance with practical protocols for prescribing and implementing PA programs to support RTW in breast cancer survivors

Le sujet de cette these concerne l'automatisation des preuves inductives de specifications et de la synthese de programmes recursifs. Plus precisement, nous avons focalise nos travaux sur les preuves de formules de la forme pour tout x, il existe y tel que phi(x,y) dans le modele initial d'un systeme equationnel. Ces formules representent des specifications de problemes. La difficulte d'une telle approche provient du fait que de telles preuves necessitent en general plus qu'un simple raisonnement equationnel et ont recours a des raisonnements inductifs. Elles sont de plus rarement automatiques. Le processus automatique que nous decrivons utilise le concept d'ensemble test d'un systeme de reecriture qui capture la notion de preuve par recurrence. Il permet alors de decomposer les preuves suivant des schemas de recurrence en preuves de lemmes plus simples, et cela d'une maniere automatique. Nous avons etendu le processus pour permettre de simplifier des egalites en utilisant l'injectivite des symboles de fonction, et pour traiter le cas des formules purement existentielles. En outre nous donnons un critere suffisant pour refuter des formules non valides dans le modele initial. Notre contribution a la synthese de programmes se place dans le cadre de l'approche constructive. Notre processus de synthese consiste a extraire le programme desire de la preuve obtenue par notre processus de preuve. Nous avons prouve la correction des programmes synthetises vis a vis de la specification et de la theorie considerees. Quant a la terminaison elle est garantie par la nature de l'ordre utilise dans la preuve. Ces methodes ont ete implantees dans le systeme lemma qui synthetise des programmes logiques. Il a permis de construire automatiquement des programmes dans des domaines comme les entiers et les listes

Les travaux de theorie de la demonstration axes sur le lambda-calcul type nous donnent la possibilite de construire des systemes de synthese de programmes a partir de preuves formelles de specifications. L'interet des systemes developpes dans ce contexte est que les programmes qui y sont obtenus sont corrects. Les auteurs de cette these utilisent un systeme de lambda-calcul type dans lequel, pour obtenir un programme qui calcule une fonction, il suffit de prouver que celle-ci est totale sur son domaine. Apres avoir presente le cadre general dans lequel ils travaillent (la theorie de types recursifs), les auteurs proposent une methode de preuve par recurrence pour les enonces de totalite de fonctions equationnellement definies. Ils donnent ensuite deux strategies automatiques de recherche de preuves conformes a cette methode et demontrent que toutes deux sont correctes et completes. La difference essentielle entre ces deux strategies est le principe de recurrence utilise. Autour de ces strategies, les auteurs ont implemente un systeme de programmation par preuve se presentant comme un langage de programmation fonctionnelle

Cette these s'interesse au probleme de la certification de programmes fonctionnels. Nous etudions une approche tres particuliere. Il est bien connu qu'une preuve mathematique constructive d'une formule affirmant l'existence d'un objet satisfaisant une certaine propriete peut s'interpreter comme une methode effective de construction de l'objet. Dans cette approche, la specification du programme est representee par une formule logique et developper le programme correspond a prouver cette formule. Il existe differentes methodes pour extraire de la preuve mathematique la partie calculatoire qui represente le programme qui, de part sa methode de construction, est certifie correct. Cette these s'interesse au probleme inverse de l'extraction de programme, a savoir etant donnes une specification et un programme, reconstruire une preuve de la specification dont le contenu algorithmique correspond au programme donne. Ce probleme n'est evidemment pas decidable. Le mieux que l'on puisse esperer est d'engendrer un certain nombre d'obligations de preuves portant sur des parties atomiques du programme et correspondant aux proprietes logiques qui doivent etre verifiees. Meme ce but ne peut etre atteint. En effet, la preuve du programme necessite en general de connaitre les proprietes intermediaires des sous-programmes qui peuvent etre plus fortes que la specification initiale. Cette these etudie d'abord une methode d'extraction faible d'un programme a partir d'une preuve qui garde trace des specifications intermediaires. A partir d'un tel programme, on montre qu'il est deterministe de retrouver les obligations de preuves minimales. Ensuite, des methodes heuristiques sont proposees pour retrouver la preuve a partir d'un programme naturel ne comportant que des annotations partielles. Finalement, la these presente la mise en uvre de cette methode comme tactique de l'assistant de preuve coq qui a permis le developpement de differents exemples dont des programmes de tri

Ce travail a pour propos la synthèse de propriétés de programmes logiques pour la transformation par pliage et dépliage. L'objectif général est l'amélioration de l'efficacité des programmes logiques par application des transformations. Le domaine de notre étude est celui des méthodes de développement formel de programmes. L'expérience et l'étude rigoureuse d'exemples montrent que les transformations par pliage et dépliage ne suffisent pas pour obtenir de manière systématique des programmes plus efficaces: il est utile de disposer et d'appliquer des propriétés qui sont des formules logiques particulières pouvant être déduites des clauses formant le programme. Le travail que nous avons réalisé s'articule autour de ces axes: 1) l'intégration de l'application de propriétés en tant que stratégies; 2) l'étude des techniques qui permettent de construire automatiquement des propriétés; en effet la découverte de propriétés est un point crucial qui marque souvent la limite de l'automatisation d'un système; 3) la preuve des propriétés découvertes. Nous avons montré que la découverte des propriétés peut être partiellement automatisé. La démarche générale consiste à mettre en évidence des classes particulières de programmes caractérisées par des modes entrée-sortie et des types. Les modes permettent d'orienter les spécifications en distinguant les données des résultats. Des techniques heuristiques ont été développées à partir de ces caractérisations. Elles permettent dans de nombreux cas de découvrir des propriétés intéressantes. Plus précisément, la stratégie proposée est basée sur l'analyse statique du programme transformé et utilise un mécanisme de projection. Nous avons étudié le problème de dépliage, ce problème est lié à la transformation de programmes logiques guidée par des schémas d'induction. Nous présentons quelques résultats théoriques liés à ce problème.

Recherche de nouvelles méthodes de synthèse logique sur différentes cibles technologiques: PLA détaillé libre et PLD de type PAL. Une méthode originale de minimisation deux couches d'un ensemble de fonctions booléennes sur une cible de type PLA libre est étudiée. Une méthode de synthèse sur les réseaux programmables de type PAL, dont les dimensions et les structures sont figées, est aussi proposée

Avec la complexité croissante des circuits VLSI, la recherche de méthodes formelles de conception de circuits devient nécessaire pour atteindre l'objectif de circuits zéro-défaut dans les délais escomptés. Dans le cadre des circuits digitaux synchrones, nous proposons une méthodologie de conception de circuits descendante par transformations de programmes. La transformation de programmes consiste à dériver une réalisation à partir de sa spécification comportementale de haut niveau. La synthèse de circuits par transformations de programmes qualifie ce processus de réalisation. Pour cela, nous avons choisi deux langages: l'un pour spécifier le comportement d'un circuit et l'autre pour décrire sa réalisation. Ces deux langages sont des sous-langages du langage purement fonctionnel Miranda. Un circuit digital est spécifié à un niveau comportemental pur. Chaque transformation produit une nouvelle description, équivalente à celle de départ. A une certaine étape des transformations, la forme de la spécification prend un sens en terme de circuit. Cette forme est obtenue par application de transformations particulières que sont le schéma d'introduction de flots ou le théorème de réalisation. Les transformations suivantes ont pour but d'optimiser le circuit. Une réalisation de circuit ainsi obtenue est correcte par construction. Une preuve a posteriori n'est donc pas nécessaire. La première partie de cette thèse présente une étude bibliographique des recherches qui ont été effectuées dans le domaine de la conception de circuits digitaux zéro défaut. La seconde partie propose une méthodologie de conception de circuits digitaux synchrones, un langage de description de circuits, des schémas de transformations et une stratégie de leur application. Enfin un ensemble d'exemples de synthèse de circuits est donné.

Les systemes de preuves bases sur les theories des types offrent un cadre uniforme qui permet de programmer, specifier et prouver. L'utilisateur dispose d'un langage de programmation, d'un langage de specification et d'outils qui l'aident a raisonner formellement sur son programme. Dans le but de rapprocher dans ces systemes la syntaxe des definitions de fonctions de celle des mathematiques et des langages de programmation a la ml, nous etudions les preuves de terminaison de fonctions recursives definies equationnellement. A partir de la methode de synthese de preuves proposee par gilles dowek pour les systemes de types purs, et celle proposee par hassan saidi pour le systeme t de godel, nous proposons une methode de synthese de preuves pour le calcul des constructions inductives (cci). Ce calcul est une theorie des types tres riche, avec types polymorphes, types dependants et types inductifs primitifs (par exemple, les types algebriques et les predicats inductifs). Cette methode est complete, et fournit un cadre general ou definir des strategies de recherche de preuves. La completude se paye par la non terminaison. Nous etudions donc des restrictions qui terminent et qui permettent de resoudre une certaine classe de problemes de filtrage et d'unification du second ordre dans cci. Nous analysons aussi la derivation de principes d'analyse par cas specialises (dits principes d'inversion), technique necessaire pour resoudre une classe large de problemes de filtrage. Ces restrictions, que l'on peut considerer comme des algorithmes de compilation, synthetisent des preuves explicites a partir de notations plus implicites, dans l'esprit de la compilation des motifs dans un langage fonctionnel. Ceci permet d'incorporer au langage de specification du systeme de preuves la notation par filtrage de motifs aussi bien pour ecrire des programmes que des preuves.

Les revues systématiques sont des outils indispensables à la synthèse des connaissances en évaluation thérapeutique. Il est désormais fréquent que plusieurs traitements soient disponibles pour une même indication. L’objectif des patients et des cliniciens est alors de savoir quels sont, parmi l’ensemble des traitements disponibles, le(s) meilleur(s). Compte tenu de la nécessité de synthétiser les données disponibles pour tous les traitements et de maintenir cette synthèse à jour, notre objectif était d’évaluer les limites du système actuel de synthèse et de développer une méthodologie alternative. Nous avons d’abord évalué la capacité des revues systématiques à prendre en compte l’ensemble des preuves disponibles sur l’effet des multiples traitements. Nous avons utilisé l’exemple des traitements de deuxième ligne du cancer bronchique non à petites cellules métastatique non muté pour EGFR ou de statut inconnu. Nous avons montré que les 29 revues systématiques publiées jusque 2015 sur cette question, considérées collectivement, fournissaient une synthèse fragmentée et non à jour de la preuve disponible. Au moins 40% des 77 essais, des 45 traitements, des 54 comparaisons de traitements et des 28 636 patients n’étaient constamment pas pris en compte dans les revues systématiques. Nous avons discuté les raisons pour lesquelles le système de synthèse des données actuel ne permettait pas de couvrir l’ensemble des données disponibles. Nous avons ensuite développé une nouvelle forme de synthèse de la preuve disponible au cours du temps, la méta-analyse en réseau cumulative et dynamique. Elle consiste à passer d’une série de méta-analyses à une méta-analyse en réseau unique, incluant l’ensemble des traitements disponibles pour une indication donnée, avec une mise à jour du réseau d’essais et de la synthèse des données dès que les résultats d’un nouvel essai deviennent disponibles. Elle débute par une méta-analyse en réseau initiale suivie d’une succession de mises à jour répétées à intervalles réguliers. Nous avons décrit les étapes méthodologiques, et développé le protocole d’une étude de preuve de concept, appliquée aux traitements de deuxième ligne du cancer bronchique non à petites cellules. Enfin, nous avons réalisé la méta-analyse en réseau initiale sur ce même exemple. Nous avons inclus 98 essais randomisés évaluant 60 traitements chez 34 179 patients. Nous avons montré que les traitements par immunothérapie (nivolumab et pembrolizumab) avaient un effet sur la survie globale supérieur aux chimiothérapies et thérapeutiques ciblées actuellement recommandées (nivolumab versus docetaxel HR=0,68 (IC95% 0,55-0,83) ; versus pemetrexed HR=0,65 (0,5-0,83) ; versus erlotinib HR=0,66 (0,51-0,84) and versus gefitinib HR=0,65 (0,51-0,82)). Les résultats étaient similaires pour le pembrolizumab. Pour la survie sans progression, le nivolumab avait aussi un effet supérieur aux quatre traitements recommandés. La méta-analyse en réseau cumulative et dynamique pourrait devenir l’outil permettant de changer de paradigme dans la synthèse des connaissances afin d’améliorer la prise de décision médicale
Systematic reviews are essential tools to synthesize available evidence for therapeutic evaluation. Multiple treatments are now frequently available for a given condition. Patients and physicians want to know which one is the best among all treatments. Thus we need to retrieve and synthesize all available evidence across all treatments and furthermore to maintain it updated when new evidence and new treatments become available. Our objective was to evaluate the limits of the current ecosystem of evidence synthesis and to develop an alternative methodology. We have first assessed the capacity of systematic reviews to cover all available evidence of multiple treatments. We took the example of second-line treatments of advanced non-small cell lung cancer with EGFR wild-type or unknown status. We have shown that the 29 systematic reviews published in this condition up to 2015, considered collectively, failed to provide a complete and updated synthesis of all available evidence. Almost 40% of the 77 trials, of the 45 treatments, of the 54 treatment comparisons and of the 28,636 patients were always missing from systematic reviews. We have discussed the reasons why the ecosystem of evidence synthesis fails to encompass all available evidence. We then developed a new paradigm to synthesize evidence over time called live cumulative network meta-analysis. This new concept consists in switching from a series of standard meta-analyses to a single network meta-analysis covering all treatments and systematically updated as soon as the results of a new trial become available. Live cumulative network meta-analysis is initiated with a network meta-analysis which is iteratively updated. We have described the methodological steps, developed the protocol of a proof-of-concept study applied to second-line treatments of advanced non-small cell lung cancer. Finally, we have performed the initial network meta-analysis in this condition. We have included 98 trials including 34,179 patients and assessing 60 treatments. We have shown that nivolumab was more effective in term of overall survival compared to docetaxel HR=0.68 (IC95% 0.55-0.83), to pemetrexed HR=0.65 (0.5-0.83), to erlotinib HR=0.66 (0.51-0.84) and to gefitinib HR=0.65 (0.51-0.82). Similar results were found with pembrolizumab. In progression free survival, nivolumab had a more important treatment effect compared to the four recommended treatments. Live cumulative network meta-analysis should become a paradigmatic shift for systematic reviews and meta-analysis in order to improve medical decision making