DeepSeek hat im Bereich des mathematischen Theorembeweises ein spezialisiertes Modell namens Prover-V2 veröffentlicht. Ziel ist es, mit KI automatisch mathematische Theoreme im formalen Verifikationssystem Lean 4 zu beweisen.
Warum ist diese Richtung wichtig?
Der mathematische Theorembeweis ist ein extremes Testfeld für die Fähigkeiten von KI. Denn die Mathematik akzeptiert kein "ungefähr richtig" – ein Beweis ist entweder vollständig korrekt oder falsch. Es gibt kein "zu 95 % richtiges Beweisstück".
Formale Verifikationssysteme (wie Lean 4) prüfen jeden Schritt der logischen Schlussfolgerung so, wie ein Compiler die Syntax prüft. Ist ein Schritt falsch, meldet der gesamte Beweis einen Fehler. Dies ist die strengste Prüfung für die logische Schlussfolgerungsfähigkeit von KI.
Die Leistung von Prover-V2
Im miniF2F-Benchmark erzielte Prover-V2 Ergebnisse, die nahe an oder auf dem Niveau der aktuell besten Ergebnisse liegen. Die verwendete Methode ist die Teilzielzerlegung – ein komplexer Beweis wird in eine Reihe kleinerer Teilziele zerlegt, die nacheinander gelöst werden.
Dies ähnelt stark der Denkweise menschlicher Mathematiker: Vor einem schwierigen Problem überlegt man zuerst: "Um A zu beweisen, muss ich zuerst B und C beweisen, und um B zu beweisen, muss ich zunächst D bestätigen …"
Unterschied zu allgemeinen Schlussfolgerungsmodellen
Allgemeine Modelle (GPT, Claude, Gemini) stützen sich beim mathematischen Schlussfolgern auf Chain-of-Thought – im Wesentlichen ein "schrittweises Vorgehen in natürlicher Sprache". Diese Methode funktioniert bei einfachen Problemen gut, aber bei komplexen Beweisen können leicht an einem Schritt logische Lücken auftreten.
Prover-V2 geht den formalen Weg: Jeder Schritt wird von Lean 4 verifiziert. Der Vorteil ist, dass es keine "Halluzinationen" gibt; der Nachteil ist der sehr enge Anwendungsbereich – es funktioniert nur innerhalb formaler Systeme.
Bedeutung
Der mathematische Theorembeweis ist eine scheinbar sehr nischenhafte, aber weitreichende Richtung. Wenn KI wirklich in der Lage ist, in formalen Systemen zuverlässig komplexe Theoreme zu beweisen, kann dies in Bereichen wie Softwareverifikation, Hardwareverifikation und kryptografischen Beweisen sowie einer Reihe weiterer kritischer Felder angewendet werden.
Die Investitionen von DeepSeek in diese Richtung zeigen, dass sie nicht nur bei Benchmarks für allgemeine große Modelle mithalten – sondern auch ernsthaft an grundlegenden wissenschaftlichen Werkzeugen arbeiten.
Quellenangabe: CocoLoop, DeepSeek Prover-V2 Paper