Satzauswahl für Theorembeweise durch tiefes Grapheneinbettung

Wir schlagen einen auf tiefem Lernen basierenden Ansatz für das Problem der Prämisselektion vor: die Auswahl mathematischer Aussagen, die für den Beweis einer gegebenen Vermutung relevant sind. Wir stellen eine Formel der höheren Logik als Graph dar, der invariant gegenüber Variablennamenänderungen ist, aber trotzdem alle syntaktischen und semantischen Informationen vollständig beibehält. Anschließend kodieren wir den Graph in einen Vektor mittels einer neuen Einbettungsmethode, die die Information über die Kantenreihenfolge bewahrt. Unser Ansatz erzielt Stand-der-Technik-Ergebnisse im HolStep-Datensatz und verbessert die Klassifikationsgenauigkeit von 83 % auf 90,3 %.