DeepSeek hat DeepSeek-Prover-V2 vorgestellt, ein bahnbrechendes Open-Source Large Language Model (LLM), das sorgfältig für den komplexen Bereich des formalen Theorembeweisens innerhalb des Lean 4 Frameworks entwickelt wurde. Dieses neuartige Modell nutzt eine rekursive Theorembeweis-Pipeline und die Leistungsfähigkeit des hochmodernen DeepSeek-V3 Foundation Models von DeepSeek. Lean 4, die neueste Iteration des Lean Theorem Provers, ist ein interaktiver Beweisassistent, der von Microsoft Research entwickelt wurde. Diese hochentwickelte funktionale Programmiersprache und das interaktive Theorembeweissystem ermöglichen es Mathematikern und Informatikern, formale Beweise mit unübertroffener maschinell überprüfter Verifikation zu erstellen.
Das Projekt stellt einen monumentalen Schritt dar, um die Kluft zwischen formalem und informellem mathematischen Denken zu überbrücken. Durch die Nutzung der inhärenten Fähigkeiten von Allzweck-LLMs soll der hochstrukturierte Bereich des formalen Theorembeweisens effektiv angegangen werden. Das DeepSeek-Forschungsteam geht davon aus, dass sein innovativer Ansatz die kognitiven Prozesse widerspiegelt, die menschliche Mathematiker beim Erstellen von Beweisen anwenden, indem sie komplexe Theoreme sorgfältig in besser handhabbare und verständliche Komponenten zerlegen.
Erweiterung des Evaluations-Frameworks: Einführung von ProverBench
Um die Strenge ihrer Forschung zu erhöhen, hat das DeepSeek-Team sein Evaluations-Framework mit der Einführung von ProverBench, einer völlig neuen Benchmark-Sammlung, die speziell für die umfassende Bewertung der Fähigkeiten des formalen Theorembeweisens entwickelt wurde, erheblich erweitert. Diese umfassende Sammlung dient als wertvolle Ressource für die Bewertung der Leistung von LLMs im Kontext der formalen Mathematik.
"Über die herkömmlichen Benchmarks hinaus stellen wir voller Stolz ProverBench vor, eine sorgfältig zusammengestellte Sammlung von 325 formalisierten Problemen, um unseren Bewertungsprozess zu bereichern. Diese Sammlung umfasst 15 sorgfältig ausgewählte Probleme, die direkt aus den jüngsten American Invitational Mathematics Examination (AIME)-Wettbewerben stammen, insbesondere aus den Jahren 24-25", erläuterten die Forscher.
Die Aufnahme von AIME-Problemen in das ProverBench-Dataset ist besonders bemerkenswert, da es eine Reihe von anspruchsvollen und etablierten mathematischen Problemen einführt, die in der mathematischen Gemeinschaft weithin anerkannt sind. Dies bietet eine standardisierte und rigorose Grundlage für die Bewertung der Leistung von DeepSeek-Prover-V2 und den Vergleich mit anderen Ansätzen.
Vielversprechende erste Ergebnisse: Bearbeitung von AIME-Problemen
Die ersten Ergebnisse, die aus rigorosen Tests mit diesen anspruchsvollen AIME-Problemen hervorgegangen sind, haben eine außergewöhnlich vielversprechende Leistung ihres sorgfältig entwickelten spezialisierten Theorembeweis-Modells gezeigt. Das DeepSeek-Team berichtet stolz, dass DeepSeek-Prover-V2 sein Können unter Beweis stellte, indem es beeindruckende 6 von 15 AIME-Problemen, die ihm vorgelegt wurden, erfolgreich löste. Im Vergleich dazu löste das Allzweck-DeepSeek-V3-Modell bei Anwendung von Mehrheitswahltechniken erfolgreich 8 Probleme.
Diese Ergebnisse verdeutlichen das Potenzial von sowohl spezialisierten als auch Allzweck-LLMs bei der Bearbeitung komplexer mathematischer Probleme. Während das Allzweckmodell in diesem speziellen Benchmark eine etwas höhere Erfolgsquote aufwies, demonstrierte das spezialisierte Theorembeweis-Modell seine Kompetenz im formalen mathematischen Denken.
Nachahmung der menschlichen Beweiskonstruktion: Ein Chain-of-Thought-Ansatz
"Angesichts der gut dokumentierten Herausforderungen, denen Allzweckmodelle oft begegnen, wenn sie versuchen, vollständige Lean-Beweise zu erstellen, haben wir DeepSeek-V3 strategisch angewiesen, nur eine allgemeine Beweisskizze zu erstellen und die komplizierten Details absichtlich auszulassen. Die resultierende Gedankenkette gipfelt in einem Lean-Theorem, das aus einer Sequenz von Have-Anweisungen besteht, die jeweils sorgfältig mit einem Sorry-Platzhalter abgeschlossen werden, der effektiv ein Teilziel angibt, das gelöst werden muss. Dieser innovative Ansatz spiegelt auf elegante Weise den menschlichen Stil der Beweiskonstruktion wider, bei dem ein komplexes Theorem inkrementell auf eine Sequenz besser handhabbarer Lemmata reduziert wird", erläuterte das DeepSeek-Team.
Dieser innovative Ansatz zur Erstellung von allgemeinen Beweisskizzen stimmt damit überein, wie Mathematiker oft an komplexe Beweise herangehen. Indem sich das Modell auf die Gesamtstruktur und die wichtigsten Schritte konzentriert, kann es die anschließende Verfeinerung und Vervollständigung des Beweises effektiv steuern.
Eine methodische Strategie: Individuelle Bearbeitung jeder Beweiskomponente
Das System wendet dann eine methodische und strukturierte Strategie an, um jede einzelne Komponente des Beweises zu bearbeiten. Dieser systematische Ansatz stellt sicher, dass jeder Aspekt des Beweises sorgfältig berücksichtigt und auf logische und kohärente Weise behandelt wird. Das System schafft einen hochstrukturierten Ansatz für das Theorembeweisen, der auf zuvor etablierten Ergebnissen aufbaut, um eine solide Grundlage für jeden nachfolgenden Schritt zu gewährleisten.
"Wir nutzen die von DeepSeek-V3 generierten Teilziele, um eine rekursive Lösungsstrategie anzuwenden, um jeden Zwischenschritt systematisch zu lösen. Wir extrahieren Teilzielausdrücke aus den Have-Anweisungen, um sie für die ursprünglichen Ziele in den gegebenen Problemen zu substituieren, und integrieren dann die vorhergehenden Teilziele als Prämissen. Diese Konstruktion ermöglicht es, nachfolgende Teilziele mithilfe der Zwischenergebnisse früherer Schritte zu lösen, wodurch eine stärker lokalisierte Abhängigkeitsstruktur gefördert und die Entwicklung einfacherer Lemmata erleichtert wird", erläuterten die Forscher detailliert.
Die rekursive Lösungsstrategie ist ein Schlüsselaspekt für die Fähigkeit des Systems, komplexe Beweise zu handhaben. Indem das Problem in kleinere, besser handhabbare Teilziele zerlegt wird, kann das System seine Denkfähigkeiten effektiv auf jede einzelne Komponente anwenden.
Optimierung der Rechenressourcen: Ein spezialisiertes 7B-Parameter-Modell
Um die Rechenressourcen effektiv zu optimieren und eine effiziente Verarbeitung zu gewährleisten, verwendet das System strategisch ein kleineres, hochspezialisiertes 7B-Parameter-Modell, um die zerlegten Lemmata zu verarbeiten. Dieser Ansatz ist entscheidend für die effektive Bewältigung des Rechenaufwands, der mit umfangreichen Beweissuchen verbunden ist, und stellt sicher, dass das System effizient arbeiten kann, ohne von der Komplexität des Suchraums überwältigt zu werden. Der Ansatz gipfelt letztendlich in einem automatisch abgeleiteten vollständigen Beweis, wenn alle zerlegten Schritte erfolgreich gelöst wurden.
"Der algorithmische Rahmen arbeitet in zwei verschiedenen Phasen und nutzt zwei komplementäre Modelle: DeepSeek-V3 für die Lemma-Zerlegung und ein 7B-Prover-Modell, um die entsprechenden formalen Beweisdetails zu vervollständigen", beschrieben die Forscher.
Dieser zweistufige Ansatz ermöglicht es dem System, die Stärken sowohl eines großen Allzweckmodells als auch eines kleineren spezialisierten Modells zu nutzen. Das große Modell wird verwendet, um allgemeine Beweisskizzen zu erstellen, während das kleinere Modell verwendet wird, um die Details auszufüllen und den formalen Beweis zu vervollständigen.
Synthetisierung formaler Denkdaten: Ein natürlicher Pfad
Diese sorgfältig entwickelte Architektur etabliert effektiv einen natürlichen und intuitiven Pfad zum Synthetisieren formaler Denkdaten, der High-Level-Mathematik nahtlos mit den strengen und rigorosen Anforderungen der formalen Verifikation verbindet. Diese Integration ist unerlässlich, um die Zuverlässigkeit und Vertrauenswürdigkeit der Ergebnisse des Systems zu gewährleisten.
"Wir kuratieren eine Teilmenge anspruchsvoller Probleme, die vom 7B-Prover-Modell nicht vollständig gelöst werden können, für die aber alle zerlegten Teilziele erfolgreich gelöst wurden. Durch die Zusammensetzung der Beweise aller Teilziele erstellen wir einen vollständig formalen Beweis für das ursprüngliche Problem", erklärten die Forscher.
Dieser Ansatz ermöglicht es dem System, aus seinen Fehlern zu lernen und seine Fähigkeit, komplexe Probleme zu lösen, zu verbessern. Indem das System die spezifischen Teilziele identifiziert, die Schwierigkeiten verursachen, kann es seine Bemühungen darauf konzentrieren, seine Leistung in diesen Bereichen zu verbessern.
Bedenken und Herausforderungen: Implementierungsdetails unter der Lupe
Trotz der unbestreitbaren technischen Leistungen von DeepSeek-Prover-V2 haben einige Experten auf dem Gebiet relevante Bedenken hinsichtlich bestimmter Implementierungsdetails geäußert. Elliot Glazer, ein hoch angesehener leitender Mathematiker bei Epoch AI, hat auf potenzielle Probleme hingewiesen, die weitere Untersuchungen erfordern.
Einige Bedenken bezüglich des DeepSeek-Prover-V2-Papers. Potenziell falsch formalisierte Beispiele, und Diskussionen auf der Lean Zulip legen nahe, dass die PutnamBench-Beweise Unsinn sind und ein implizites Sorry verwenden (möglicherweise versteckt in der Apply?-Taktik), das in ihrer Read-Eval-Print-Loop nicht gemeldet wird.
Diese Bedenken verdeutlichen die anhaltenden Herausforderungen im Bereich der formalen Verifikation, in dem selbst die kleinsten und scheinbar unbedeutenden Implementierungsdetails einen überproportional großen Einfluss auf die Gesamtgültigkeit und Zuverlässigkeit der Ergebnisse haben können. Der formale Verifikationsprozess erfordert unerschütterliche Aufmerksamkeit für Details und die sorgfältige Einhaltung etablierter Standards.
Das Potenzial für falsch formalisierte Beispiele und die Möglichkeit versteckter "Sorry"-Taktiken in den PutnamBench-Beweisen werfen wichtige Fragen hinsichtlich der Strenge und Vollständigkeit des Verifikationsprozesses auf. Diese Bedenken unterstreichen die Notwendigkeit einer fortgesetzten Prüfung und unabhängigen Verifizierung der Ergebnisse.
Verfügbarkeit und Ressourcen: Demokratisierung des Zugangs zum formalen Theorembeweisen
DeepSeek hat seinen Prover-V2 in zwei verschiedenen Modellgrößen verfügbar gemacht, um einer Vielzahl von Rechenressourcen und Forschungszielen gerecht zu werden. Die erste Version ist ein 7B-Parameter-Modell, das auf ihrem vorherigen Prover-V1.5-Base basiert und eine erweiterte Kontextlänge von bis zu 32K Token aufweist. Die zweite Version ist ein deutlich größeres 671B-Parameter-Modell, das auf DeepSeek-V3-Base trainiert wurde. Beide Modelle sind jetzt auf HuggingFace, einer führenden Plattform für das Teilen und Zusammenarbeiten von Modellen des maschinellen Lernens, leicht zugänglich.
Zusätzlich zu den Modellen selbst hat DeepSeek auch das vollständige ProverBench-Dataset, das 325 sorgfältig formalisierte Probleme zu Bewertungszwecken enthält, auf HuggingFace verfügbar gemacht. Dieses umfassende Dataset bietet Forschern und Entwicklern eine wertvolle Ressource, um die Leistung ihrer Modelle zu bewerten und sie mit DeepSeek-Prover-V2 zu vergleichen.
Indem DeepSeek diese Ressourcen frei verfügbar macht, demokratisiert es den Zugang zur Technologie des formalen Theorembeweisens und fördert die Zusammenarbeit innerhalb der Forschungsgemeinschaft. Dieser Open-Source-Ansatz dürfte den Fortschritt auf diesem Gebiet beschleunigen und zu neuen Durchbrüchen im Bereich des automatisierten Denkens und der Verifikation führen.
Diese Veröffentlichung stattet Forscher und Entwickler mit den Ressourcen aus, die sie benötigen, um die Fähigkeiten und Grenzen dieser Technologie zu untersuchen. Durch die Bereitstellung eines offenen Zugangs zu den Modellen und dem ProverBench-Dataset fördert DeepSeek weitere Erkundungen und gemeinsame Anstrengungen, um die von Experten auf dem Gebiet geäußerten Bedenken auszuräumen. Dieser kollaborative Ansatz ist der Schlüssel, um die Komplexitäten des formalen Theorembeweisens zu entschlüsseln und die Zuverlässigkeit dieser bahnbrechenden Fortschritte zu festigen.