Graphendarstellungen für höhere Ordnung Logik und Theorembeweisung

Dieses Papier präsentiert die erste Anwendung von Graph Neural Networks (GNNs) für die höherstufige Beweissuche und zeigt, dass GNNs die aktuellen besten Ergebnisse in diesem Bereich verbessern können. Interaktive, höherstufige Theorembeweiser ermöglichen es, die meisten mathematischen Theorien formal zu gestalten, und stellen eine erhebliche Herausforderung für tiefes Lernen dar. Die höherstufige Logik ist hochgradig ausdrucksstark und obwohl sie gut strukturiert ist, mit einer klar definierten Grammatik und Semantik, gibt es bislang keine etablierte Methode zur Umwandlung von Formeln in graphbasierte Darstellungen. In dieser Arbeit betrachten wir verschiedene graphische Darstellungen der höherstufigen Logik und bewerten sie anhand des HOList-Benchmarks für den Beweis höherstufiger Theoreme.