SATNet: Die Brücke zwischen tiefem Lernen und logischem Schließen durch einen differenzierbaren Erfüllbarkeitssolver

Die Integration logischen Schließens in tiefen Lernarchitekturen ist ein wichtiges Ziel moderner KI-Systeme. In dieser Arbeit schlagen wir eine neue Richtung zu diesem Ziel vor, indem wir einen differenzierbaren (verglätten) Maximalerfüllbarkeitslöser (Maximum Satisfiability Solver, MAXSAT) einführen, der in den Kreislauf größere tiefer Lernsysteme integriert werden kann. Unser (näherungsweiser) Löser basiert auf einem schnellen Koordinatenabstiegsverfahren zur Lösung des dem MAXSAT-Problem zugeordneten semidefiniten Programms (SDP). Wir zeigen, wie man die analytische Differenzierung durch die Lösung dieses SDPs durchführen und den damit verbundenen Rückwärtsdurchgang effizient lösen kann. Wir demonstrieren, dass die Integration dieses Löasers in end-to-end-Lernsysteme es ermöglicht, die logische Struktur anspruchsvoller Probleme mit minimaler Überwachung zu erlernen. Insbesondere zeigen wir, dass wir die Paritätsfunktion unter Verwendung von Einbit-Überwachung (eine traditionell schwierige Aufgabe für tiefe Netze) und lernen können, 9x9-Sudoku allein aus Beispielen zu spielen. Darüber hinaus lösen wir ein "visuelles Sudoku"-Problem, das Bilder von Sudoku-Rätseln auf ihre entsprechenden logischen Lösungen abbildet, indem wir unseren MAXSAT-Löser mit einer traditionellen Faltungsarchitektur kombinieren. Unser Ansatz zeigt daher vielversprechende Ergebnisse bei der Integration logischer Strukturen in tiefes Lernen.