Vampires can Lean into trust: checking proofs for soundness

Abstract

Moderne automatische Theorembeweiser (ATPs) wie Vampire sind große Programme, die symbolisches Schließen für ein breites Anwendungsspektrum ermöglichen, darunter Softwareanalyse, die Formalisierung von Mathematik und Cybersicherheit. Obwohl der zugrunde liegende Kalkül von Vampire als korrekt bewiesen ist, kann dessen Implementierung Fehler enthalten, die zu inkorrekten Beweisen führen können. Diese Arbeit präsentiert eine Methode, um das Vertrauen in solche Beweise zu erhöhen, indem ihre Korrektheit vollständig überprüft wird. Dazu werden die von Vampire erzeugten Beweise in eine Form übersetzt, die mit dem interaktiven Theorembeweiser Lean geprüft werden kann. Die vorgestellte Methode unterstützt die CNF- (clause normal form) und FOF- (first-order form) Fragmente der Prädikatenlogik erster Stufe mit Gleichheit. Um eine vollständige Beweisprüfung einschließlich der Vorverarbeitung (Preprocessing) zu ermöglichen, werden in dieser Arbeit zwei Änderungen an Vampire bezüglich der Skolemisierung und der Behandlung purer Prädikate eingeführt und separat evaluiert.Darüber hinaus wird eine Methode des “proof replay” in Vampire vorgestellt, die während der Beweissuche aus Performanzgründen verworfene Beweisdetails rekonstruiert, welche jedoch für eine effiziente Rekonstruktion der Beweise in Lean relevant sind. Die Möglichkeit, einen Beweis vollständig durch den vertrauenswürdigen Kernel von Lean zu überprüfen, stellt eine erhebliche Steigerung des Vertrauens in die von Vampire generierten Beweise dar. Dadurch werden solche Beweise insbesondere für sicherheitskritische Anwendungen, aber auch für die weiteren Einsatzgebiete von Vampire noch wertvoller.Die vorgestellte Methode wird auf einem großen Satz von Benchmark-Problemen (TPTP 9.2.1) evaluiert und zeigt, dass 99% der von Vampire (unter einem Instruktionslimit von 100 Giga-Instruktionen) gefundenen Beweise mit einem Zeitlimit von 1000 s erfolgreich in Lean geprüft werden konnten. Außerdem wurden zwei weitere, weniger spezialisierte Ansätze zur Beweisprüfung unter Verwendung eines externen beweisproduzierenden ATPs (Duper) evaluiert, die den Performanzvorteil der vorgestellten Methode demonstrieren.

Modern automated theorem provers (ATPs) such as Vampire are large programs that provide symbolic reasoning capabilities for a wide range of applications, including software analysis, the formalization of mathematics, and cybersecurity. While the underlying calculus of Vampire is known to be sound, its implementation may contain bugs that can lead to unsound proofs. This thesis presents a method to increase trust in these proofs by verifying their soundness end-to-end, translating them into a form that can be checked using the interactive theorem prover (ITP) Lean. The presented ap proach applies to the CNF (clause normal form) and FOF (first-order form) fragments of first-order logic with equality. To achieve full proof checking including preprocessing, this work introduces two modifications concerning skolemization and the handling of pure predicates in Vampire and evaluates them separately. Furthermore, it introduces a “proof-replay” method in Vampire that reconstructs proof details discarded during proof search for performance reasons, but relevant for efficient proof reconstruction in Lean. The ability to check a proof end-to-end by a trusted kernel in Lean is a significant increase in trust in the proofs generated by Vampire, which makes such proofs even more valuable for safety-critical applications as well as in the other application domains of Vampire.The presented method is evaluated on a large benchmark set (TPTP 9.2.1), showing that 99% of proofs found by Vampire (within an instruction limit of 100 giga-instructions) could be successfully checked in Lean with a time limit of 1000 s. Furthermore, two other, less specialized, approaches to proof checking using an external proof-producing ATP (Duper) were evaluated and compared against the developed method, demonstrating the performance benefit of the proposed approach.