Große Sprachmodelle (LLMs) haben bedeutende Fortschritte in mathematischer Argumentation und Theorembeweisen gemacht, stehen jedoch vor erheblichen Herausforderungen bei formalen Theorembeweisen mit Systemen wie Lean und Isabelle. Diese Systeme erfordern strenge Ableitungen, die sich strengen formalen Spezifikationen anpassen müssen, was selbst für fortschrittliche Modelle wie GPT-4 Schwierigkeiten bereitet. Die Kernherausforderung besteht darin, dass das Modell gleichzeitig die Syntax und Semantik formaler Systeme verstehen muss, während abstrakte mathematische Argumentationen mit präzisen formalen Darstellungen übereinstimmen müssen. Dies erfordert ein tiefgehendes Verständnis von Codierungsfeinheiten und mathematischen Konzepten, was aktuelle KI-Systeme vor erhebliche Hürden bei der Erstellung komplexer formaler Beweise stellt.
Forscher von DeepSeek-AI stellten DeepSeek-Prover-V1.5 vor, einen vereinten Ansatz, der die Stärken von Proof-Step und Whole-Proof-Generierungstechniken durch einen robusten Truncate-and-Resume-Mechanismus kombiniert. Diese Methode beginnt mit der Whole-Proof-Generierung, bei der das Sprachmodell den vollständigen Beweiscode basierend auf der Theoremaussage produziert. Der Lean-Beweiser überprüft dann diesen Code. Wenn ein Fehler erkannt wird, wird der Code bei der ersten Fehlermeldung abgeschnitten, und der erfolgreich generierte Teil dient als Eingabe für das nächste Beweissegment. Der neueste Stand des Lean 4-Beweisers wird als Kommentar zur Eingabe hinzugefügt, um die Genauigkeit zu verbessern. Der Truncate-and-Resume-Mechanismus ist in die Monte-Carlo-Tree-Suche (MCTS) integriert, die flexible Abschneidpunkte ermöglicht, die durch die Tree-Search-Richtlinie festgelegt werden. Außerdem wird ein Reward-freier Explorationsalgorithmus vorgeschlagen, um das Problem der spärlichen Belohnungssuche zu lösen, der dem Tree-Search-Agenten intrinsische Motivation für eine umfassende Exploration des Taktikzustandsraums zuweist.
Diese Studie präsentiert die folgenden Beiträge: Vor-Training des verbesserten Basismodells mit weiterem Training in Mathematik und Code-Daten, Fokussierung auf formale Sprachen wie Lean, Isabelle und Metamath. Supervised Fine-Tuning verbesserte Lean 4-Code-Vervollständigungsdatensatz durch zwei Datenvermehrungstechniken: Verwendung von DeepSeek-Coder V2 236B zur Hinzufügung von natürlichsprachlichen “Chain-of-Thought”-Kommentaren und Einfügen von Zwischenstatusinformationen innerhalb des Lean 4-Beweiscodes. Einsatz des GRPO-Algorithmus für das Reinforcement-Learning vom Proof Assistant-Feedback (RLPAF), unter Verwendung der Lean-Beweisergebnisse als Belohnungen. Fortgeschrittene Tree-Search-Methode mit Truncate-and-Resume-Mechanismus als Zustandsaktionsabstraktion, RMaxTS-Algorithmus unter Verwendung der RMax-Strategie für die Exploration in der spärlich belohnten Beweissuche und Zuteilung intrinsischer Belohnungen zur Förderung verschiedener Planungspfade und umfassender Beweisraumerkundungen.
DeepSeek-Prover-V1.5, ein 7-Milliarden-Parameter-Sprachmodell, setzt neue Maßstäbe in der formalen Theorembeweisführung unter Verwendung von Lean 4. Auf DeepSeek-Prover-V1.5-Base aufbauend, unterzieht es sich speziellem Vor-Training, umfassendem Supervised Fine-Tuning und Reinforcement-Learning über GRPO. Das Modell integriert RMaxTS, eine innovative Variante der Monte-Carlo-Tree-Suche, um Problemlösungen durch umfassende Exploration zu verbessern. Dieses Framework etabliert einen AlphaZero-ähnlichen Ablauf für formale Theorembeweise, unter Verwendung von Experteniteration und synthetischen Daten. Während der aktuelle Fokus auf der Exploration liegt, könnten zukünftige Entwicklungen einen Kritikermodell für die Bewertung unvollständiger Beweise umfassen, um den Ausbeutungsaspekt des Reinforcement-Learning bei Theorembeweisen anzugehen.