Zerlegung des Rätsels: subgoalbasiertes Demonstrationslernen für formale Beweisführung

Große Sprachmodelle (LLMs) eröffnen im Bereich des formalen Beweisens eine vielversprechende Forschungsperspektive. Dennoch bleibt die vollständige Ausnutzung dieser Modelle, insbesondere hinsichtlich der Formatierung und Strukturierung von Beweisbeispielen, ein bisher wenig erforschtes Gebiet. Um die Effektivität von LLMs zu steigern, stellen wir einen subgoal-basierten Ansatz für das Lernen anhand von Demonstrationen vor, der aus zwei zentralen Komponenten besteht: Erstens nutzen wir Erkenntnisse aus dem Bereich des Subgoal-Lernens in der Verstärkungslern- und Robotikforschung, um für jedes Beweisbeispiel spezifische Teilziele zu definieren und diese anhand der relevanten Theorien des Subgoal-Lernens zu verfeinern. Zweitens bauen wir auf jüngste Fortschritte bei Diffusionsmodellen auf, um die optimale Organisation von Beweisbeispielen vorherzusagen und gleichzeitig zwei komplexe Herausforderungen im Bereich der Demonstrationsoptimierung zu lösen: die Auswahl relevanter Teilmengen und die Bestimmung der richtigen Reihenfolge. Durch die Integration subgoal-basierter Lernmethoden konnten wir die bisher beste Beweisgenauigkeit auf dem miniF2F-Benchmark von 38,9 % auf 44,3 % steigern. Darüber hinaus führt die Anwendung von Diffusionsmodellen zur Organisation von Demonstrationen zu einer weiteren Genauigkeitssteigerung auf 45,5 %, oder einer um das Fünffache verbesserten Sampling-Effizienz im Vergleich zur langjährigen State-of-the-Art-Methode. Unser Quellcode ist unter \url{https://github.com/HKUNLP/subgoal-theorem-prover} verfügbar.