Satzbeweise erlernen durch Interaktion mit Beweisassistenten

Menschen beweisen Sätze, indem sie sich auf erhebliche hochstufige Denkprozesse und problemspezifische Erkenntnisse stützen. Beweisassistenten bieten eine Formalisierung, die der menschlichen mathematischen Denkweise ähnelt, indem sie Sätze in höherstufiger Logik darstellen und Beweise als hochstufige Taktiken modellieren. Allerdings müssen menschliche Experten die Beweise manuell durch Eingabe von Taktiken in den Beweisassistenten konstruieren. In dieser Arbeit untersuchen wir das Problem der Automatisierung der Interaktion mit Beweisassistenten mithilfe des maschinellen Lernens. Wir erstellen CoqGym, eine umfangreiche Datenbank und Lernumgebung, die 71.000 menschlich verfasste Beweise aus 123 Projekten enthält, die mit dem Coq-Beweisassistenten entwickelt wurden. Wir entwickeln ASTactic, ein auf tiefem Lernen basierendes Modell, das Taktiken als Programme in Form abstrakter Syntaxbäume (ASTs) generiert. Experimente zeigen, dass ASTactic, das auf CoqGym trainiert wurde, effektive Taktiken generieren kann und verwendet werden kann, um neue Sätze zu beweisen, die bisher nicht durch automatische Methoden bewiesen werden konnten. Der Quellcode ist unter https://github.com/princeton-vl/CoqGym verfügbar.