Lernen von Schlussfolgerungsstrategien im end-to-end differenzierbaren Beweisen

Versuche, tiefe Lernmodelle interpretierbar, dateneffizient und robust zu gestalten, haben durch die Hybridisierung mit regelbasierten Systemen einige Erfolge erzielt, beispielsweise bei neuronalen Theorembeweisern (Neural Theorem Provers, NTPs). Diese neuro-symbolischen Modelle können interpretierbare Regeln induzieren und über Rückpropagation Darstellungen aus Daten lernen, während sie gleichzeitig logische Erklärungen für ihre Vorhersagen liefern. Sie sind jedoch durch ihre rechnerische Komplexität eingeschränkt, da sie alle möglichen Beweispfade berücksichtigen müssen, um ein Ziel zu erklären, was sie für großskalige Anwendungen ungeeignet macht. Wir stellen bedingte Theorembeweiser (Conditional Theorem Provers, CTPs) vor, eine Erweiterung von NTPs, die über gradientenbasierte Optimierung eine optimale Strategie zur Regelauswahl lernt. Wir zeigen, dass CTPs skalierbar sind und auf dem CLUTRR-Datensatz, der die systematische Generalisierung neuronaler Modelle testet, indem es lernt, über kleinere Graphen zu schließen und auf größeren zu evaluieren, Ergebnisse auf dem Stand der Technik erzielen. Schließlich zeigen CTPs im Vergleich zu anderen neuro-symbolischen Modellen bessere Ergebnisse bei der Link-Vorhersage auf etablierten Benchmarks, wobei sie gleichzeitig interpretierbar bleiben. Der gesamte Quellcode und die Datensätze sind online verfügbar unter https://github.com/uclnlp/ctp.