LEGO-Prover: Neuronales Theorembeweisen mit wachsenden Bibliotheken

Trotz des Erfolgs großer Sprachmodelle (LLMs) bleibt die Aufgabe des Beweisens von Sätzen eine der schwierigsten Schlussfolgerungsaufgaben, die weit davon entfernt ist, vollständig gelöst zu sein. Vorherige Methoden, die Sprachmodelle einsetzen, haben vielversprechende Ergebnisse erzielt, stoßen jedoch weiterhin an ihre Grenzen, wenn es darum geht, selbst Schulniveau-Sätze zu beweisen. Ein häufiger Limitation dieser Ansätze ist die Annahme einer festen Satzbibliothek während des gesamten Beweisprozesses. Doch wie wir alle wissen, ist die Erzeugung neuer, nützlicher Sätze – ja sogar ganzer Theorien – nicht nur hilfreich, sondern entscheidend und unerlässlich für den Fortschritt der Mathematik und die Beweisführung komplexerer und tiefergehender Ergebnisse. In dieser Arbeit präsentieren wir LEGO-Prover, das eine wachsende Fähigkeitsbibliothek nutzt, die verifizierte Lemmata als Fähigkeiten enthält, um die Fähigkeiten von LLMs im Bereich des Satzbeweisens zu erweitern. Durch die modulare Konstruktion des Beweises ermöglicht LEGO-Prover es den LLMs, vorhandene Fähigkeiten aus der Bibliothek abzurufen und während des Beweisprozesses neue Fähigkeiten zu generieren. Diese Fähigkeiten werden anschließend (durch Prompting eines LLMs) weiterentwickelt, um die Bibliothek auf einer anderen Ebene zu bereichern. Modular und wiederverwendbare Fähigkeiten werden kontinuierlich der Bibliothek hinzugefügt, um die Bewältigung immer komplexerer mathematischer Probleme zu ermöglichen. Darüber hinaus schließt die gelernte Bibliothek die Lücke zwischen menschlichen Beweisen und formalen Beweisen, indem sie das Nachvollziehen fehlender Beweisschritte erleichtert. LEGO-Prover verbessert die Stand der Technik hinsichtlich der Erfolgsrate auf miniF2F-valid (von 48,0 % auf 57,0 %) und miniF2F-test (von 45,5 % auf 47,1 %). Während des Beweisprozesses gelingt es LEGO-Prover zudem, über 20.000 Fähigkeiten (Sätze/Lemmata) zu generieren und in die wachsende Bibliothek aufzunehmen. Unsere Ablationsstudie zeigt, dass diese neu hinzugefügten Fähigkeiten tatsächlich zur Beweisführung beitragen, wodurch sich die Erfolgsrate von 47,1 % auf 50,4 % erhöht. Außerdem veröffentlichen wir unseren Code sowie alle generierten Fähigkeiten.