Non-Linear reasoning in the superposition calculus

Abstract

Das Beweisen arithmetischer Eigenschaften hat viele Anwendungsgebiete. Diese reichen von klassischen Einsatzfällen in der Computeralgebra oder Funktionsanalyse bis hin zu angewandten Fallstudien aus dem Bereich der Softwareanalyse und Verifikation.Beispielsweise werden Operationen wie Addition, Multiplikation oder Potenzierung durch Programmschleifen über numerischen Datenstrukturen dargestellt. Während wir in der automatisierten Beweisführung mit arithmetischen Ausdrücken bereits große Fortschritte im Bereich der linearen Algebra verzeichnen können, steckt das automatisierte Beweisen nicht-lineare Eigenschaften noch in den Kinderschuhen. Obwohl dieser Teilbereich noch recht unerforscht ist, gibt es bereits SMT (Satisfiability Modulo Theory) Solver, diein nicht-linearen arithmetischen Theorien eingesetzt werden. Typischerweise, wirddie Performance solcher Solver mittels Benchmarks unterschiedlichen Schwierigkeitsgrades festgestellt. Gemessen werden dabei unterschiedliche Metriken wie (üblicherweise) das Laufzeitverhalten oder die Qualität des Ergebnisses (bspw. die Länge des erzeugten Beweises). Für nicht-lineare Arithmetik über den natürlichen oder reellen Zahlen gibt es bereits eine große Anzahl solcher Benchmarks. Zwar eignen sich diese hervorragend dazu, die Performance zu messen, doch neigen Benchmarks üblicherweise zu hoher Komplexität und sind nur schwer lesbar. Es ist daher oft schwierig aufgrund von Benchmarks Probleme im Solver zu erkennen. In dieser Arbeit beschreiben wir unterschiedliche Möglichkeiten Benchmarks zu generieren, deren Komplexität in gewisser Weise adaptierbar ist. Dabei nutzen wirBenchmarks, die ursprünglich für die automatisierte Erzeugung von Invarianten von Schleifen gedacht waren - ein wichtiger Teilbereich der automatisierten Software Verifizierung. Für viele Schleifen können solche Invarianten als Polynome überden Variablen des betrachteten Programms beschrieben werden. Sie eignen sich daherhervorragend für unsere Benchmarks im Bereich der nicht-linearen Arithmetik. Die generierten Benchmarks formulieren die Korrektheit der Invarianten in Prädikatenlogik. Zusätzlich zu den vorgestellten Methoden für die Erzeugung dieser Benchmarks liefern wir auch Beweise für deren Korrektheit. Wir zeigen daher, dass eine Invariante genau dann korrekt ist, wenn die im Benchmark formulierte prädikatenlogische Aussage eine Tautologie ist. Die bereits erwähnte Adaptionder Komplexität der Benchmarks wird durch Ausnützung bestimmter Eigenschaften von polynomiellen Invarianten erreicht. Die erzeugten Benchmarks wurden dann mittels zweier State-of-the-Art Solver getestet: Vampire und Z3. Basierend auf diesen Ergebnissen untersuchen wirden Einfluss der Adaptionen der Benchmarks auf die Performance des Solvers. Zusätzlich stellen wir weitere Vorgehensweisen zur Performance-Steigerung vor.

Proving arithmetic properties has many applications, ranging from classical use cases of computer algebra and functional analysis to more applied case studies from software analysis and verification. For example, program loops over numeric data structures naturally implement addition, multiplication and exponentiation operations. While automating reasoning about such arithmetic properties has already made significant progress in the domain of linear algebra, non-linear reasoning in the context of satisfiability and validity checking is sill at its infancy. Although this subfield of automated reasoning is still quite unexplored, there do exist SMT-solvers (satisfiability modulo theory) which are able to reason about such non-linear arithmetic properties. Whenever new proving techniques or improvements are discovered, a typical approach to evaluate their performance is to test them on challenges of varying difficulty and compare different metrics like runtime or quality of the result (e.g. length of the proof) with those of other solvers. For non-linear arithmetic over reals and over integers, a large dataset of such challenges already exists (e.g. SMT-Lib benchmarks). Although these benchmarks are well suited for performance tests, they are often complex and only theoretically readable by humans. Therefore, it usually becomes difficult to get to the real problem when a benchmark is not solved. In this thesis, we describe various ways to generate benchmarks where the complexitycan be adjusted in different ways. The benchmarks are not created from scratch but are based on challenges originally designed for loop invariant generators. For a wide range of loops, these invariants can be represented by polynomials over the variables occurring in the program, which makes them a perfect fit for our benchmarks. The benchmarks formulate a correctness claim for polynomial loop invariants in first-order logic. All the methods described in this thesis for generating such benchmarks are proven to be sound. That is, we show that the correctness claim is a valid formula if and only if the corresponding polynomial invariant is indeed an invariant of the considered loop. The already mentioned variation of the benchmark is then achieved by exploiting properties of polynomial invariants. Experiments on the generated benchmarks were then conducted, using the two state-of-the-art solvers Vampire and Z3. Based on the resultsof the experiments, we have investigated the impact of varying the complexity of the benchmarks. Additionally, we suggest further approaches and adaptions to the solver in an attempt to improve their performance