Holophrasmus: ein neuronales automatisches Theorembeweiser für höherstufige Logik

Ich schlage ein System für das automatische Beweisen von Sätzen in höherer Ordnungslogik vor, das tiefes Lernen nutzt und auf manuell konstruierte Merkmale verzichtet. Holophrasm nutzt die Formalisierung der Metamath-Sprache und untersucht partielle Beweisbäume mit einem banditenalgorithmus, der durch neuronale Netze erweitert wurde, sowie einem Sequenz-zu-Sequenz-Modell zur Aktionserzeugung. Das System beweist 14 % seiner Testsätze aus dem Modul set.mm von Metamath.