SubgoalXL: Subgoal-basiertes Expertenlernen für Beweisführung

Das formale Beweisen von Sätzen, ein Bereich an der Schnittstelle zwischen Mathematik und Informatik, hat mit den Fortschritten in großen Sprachmodellen (LLMs) erneut an Interesse gewonnen. Dieses Papier stellt SubgoalXL vor, einen neuen Ansatz, der subzielbasierte Beweise mit Expertenlernen kombiniert, um die Fähigkeiten von LLMs im formalen Beweisen innerhalb der Isabelle-Umgebung zu verbessern. SubgoalXL greift zwei entscheidende Herausforderungen auf: den Mangel an spezialisierten mathematischen und beweisorientierten Daten sowie die Notwendigkeit, die mehrstufigen Schlußfolgerungsfähigkeiten von LLMs zu steigern. Durch die Optimierung der Dateneffizienz und die Anwendung von subzielbasiertem Überwachungslernen extrahiert SubgoalXL reichere Informationen aus begrenzten menschlich generierten Beweisen. Das Framework integriert subzielorientierte Beweisstrategien in ein Expertenlernsystem und verfeinert iterativ die Generatoren für formale Aussagen, Beweise und Unterziele. Indem es die Vorteile der Isabelle-Umgebung bei subzielbasierten Beweisen nutzt, erreicht SubgoalXL eine neue Spitzenleistung von 56,1 % auf dem Standard-Datensatz miniF2F in Isabelle, was einer absoluten Steigerung von 4,9 % entspricht. Bemerkenswerterweise löst SubgoalXL erfolgreich 41 Aufgaben des American Mathematics Competitions (AMC12), 9 Aufgaben des American Invitational Mathematics Examination (AIME) und 3 Aufgaben der International Mathematical Olympiad (IMO) aus dem miniF2F-Datensatz. Diese Ergebnisse unterstreichen die Effektivität der Maximierung der Nutzwert begrenzter Daten und das Einsatz gezielter Anleitung für komplexe Schlussfolgerungen im formalen Beweisen, was zur stetigen Weiterentwicklung der KI-Schlussfolgerungsfähigkeiten beiträgt. Die Implementierung ist unter \url{https://github.com/zhaoxlpku/SubgoalXL} verfügbar.