In einer Ära, in der Künstliche Intelligenz (KI) eine immer zentralere Rolle in Wissenschaft und Technik spielt, stellt Chinas Unternehmen DeepSeek einen bedeutenden Fortschritt vor. Mit der Veröffentlichung seines neuesten Modells Prover V2 präsentiert DeepSeek ein offenes, auf Mathematik spezialisertes KI-Modell, das speziell für die Verifikation und Generierung mathematischer Beweise entwickelt wurde. Diese Entwicklung markiert nicht nur einen technologischen Meilenstein, sondern auch eine spannende Herausforderung für Branchenriesen wie OpenAI. DeepSeek hat Prover V2 am 30. April 2025 auf der renommierten Hosting-Plattform Hugging Face veröffentlicht.
Besonders hervorzuheben ist die Open-Source-Lizenzierung unter der MIT-Lizenz, die große Flexibilität und Freiheit für Entwickler und Forschende weltweit bietet. Solche offenen Modelle ermöglichen es der Gemeinschaft, Innovationen voranzutreiben und das Potenzial von Künstlicher Intelligenz breiter zugänglich zu machen. Das technische Herzstück von Prover V2 stellen seine 671 Milliarden Parameter dar. Diese beeindruckende Zahl macht es zu einem der größten KI-Modelle seiner Art auf dem Markt und übertrifft die Vorgänger Prover V1 und Prover V1.5, die bereits im August 2024 vorgestellt wurden.
Das Modell wurde speziell darauf trainiert, komplexe mathematische Wettbewerbsaufgaben in formale Logik zu übersetzen und mit Hilfe der Lean 4 Programmiersprache Beweise zu erzeugen und zu verifizieren. Lean 4 ist eine moderne, weit verbreitete Sprache, die speziell für mathematische Formalisierung und Theorembeweise entwickelt wurde. Die Fähigkeit von Prover V2, mathematisches Wissen zu komprimieren und nutzbar zu machen, kann eine Revolution im Bereich der Forschung und der Bildung auslösen. Mathematische Beweise sind oft sehr zeitintensiv und fehleranfällig. Mit dem Einsatz eines solchen KI-Modells können Wissenschaftler und Studierende signifikanter unterstützt werden, da Prover V2 Beweisschritte unterstützt, validiert und sogar neue Ansätze generiert.
Mit seinen 671 Milliarden Parametern ist Prover V2 sehr ressourcenintensiv. Die Datei des Modells hat eine Größe von circa 650 Gigabyte. Das bedeutet, dass zum Betrieb viel RAM oder VRAM, das auf Grafikprozessoren verfügbar ist, benötigt wird. Auch wenn die Hardwareanforderungen hoch sind, stellt die Verfügbarkeit des Modells als offener Download auf Hugging Face eine große Errungenschaft für die KI-Community dar. Anwender mit entsprechender technischer Ausstattung können die KI direkt lokal ausführen, ohne auf externe Server und deren Infrastruktur angewiesen zu sein.
DeepSeek hat zur Reduzierung der Modellgröße eine Quantisierung auf 8-Bit-Fließkommazahlen vorgenommen, wodurch die Parameter von 16 auf 8 Bit halbiert wurden. Diese Technik reduziert den benötigten Speicher erheblich, ohne die Genauigkeit der mathematischen Beweisführung signifikant zu beeinträchtigen. Die Kombination technischer Fortschritte wie Modell-Quantisierung und Distillation, bei der kompaktere Modelle die Leistung größerer Modelle nachahmen, öffnet die Tür für eine breitere Nutzung komplexer KI-Systeme auch auf bescheidenerer Hardware. Die Historie von DeepSeek selbst zeigt einen rasanten Fortschritt. Das erste Modell, Prover V1, basierte auf einem vergleichsweise kleinen Modell mit sieben Milliarden Parametern und war mit synthetischen Daten trainiert, also Daten, die mittels KI generiert wurden.
Prover V1.5 verbesserte dann durch Optimierungen beim Training und der Ausführung die Genauigkeit deutlich. Obwohl noch keine offiziellen Forschungspapiere zu Prover V2 veröffentlicht wurden, lässt die enorme Steigerung der Parameteranzahl und die Technologie dahinter vermuten, dass das neue Modell auf der erfolgreichen R1-Architektur von DeepSeek basiert. R1 sorgte bereits bei seiner Veröffentlichung für viel Aufsehen, da es in puncto Leistungsfähigkeit mit OpenAI´s damaligem Modell o1 konkurrieren konnte. Die offene Veröffentlichung von R1 wurde in der Szene kontrovers diskutiert.
Einerseits wurde es als wegweisender Schritt zur Demokratisierung von KI gefeiert, andererseits führten die fehlenden Sicherheitsmechanismen zum Schutz vor Missbrauch zu Bedenken und warnenden Stimmen. Über die Veröffentlichung von Prover V2 hinaus signalisiert DeepSeek damit erneut das Engagement für offene KI-Modelle. Die Bedeutung offener KI-Modelle ist nicht zu unterschätzen. Open-Source-Ansätze geben der globalen Gemeinschaft die Möglichkeit, Innovationen frei weiterzuentwickeln und Kooperationen über Grenzen hinweg zu fördern. Gleichzeitig schärfen Diskussionen um Open-Weights, also frei zugängliche Modellgewichte, die Herausforderungen hinsichtlich Sicherheit, ethischer Nutzung und Regulierung.
Für DeepSeek ist dieser Schritt einerseits ein klarer Schritt in Richtung technologische Eigenständigkeit Chinas im KI-Bereich, andererseits eine Einladung an die internationale Forschergemeinde. Ein wichtiger Aspekt bei der Verbreitung von KI-Modellen ist zudem die immer bessere Zugänglichkeit. Wegen der Komplexität und des hohen Rechenbedarfs waren LLMs (Large Language Models) lange Zeit einer kleineren Gruppe an Forschenden und Unternehmen vorbehalten. Mit Techniken wie Quantisierung, Distillation und weiteren Parametermanagement-Methoden wird es zunehmend möglich, leistungsfähige KI-Modelle auch auf weniger leistungsfähiger Hardware lokal laufen zu lassen. DeepSeek hat beispielsweise R1 in unterschiedliche Ausführungen destilliert, vom 70-Milliarden-Parameter-Modell bis hinunter zu Varianten mit nur 1,5 Milliarden Parametern.
Die kleineren Versionen können teilweise sogar mobil auf Smartphones laufen, was die Verfügbarkeit und praktische Anwendung deutlich verbessert. Die Rolle von DeepSeek in der globalen KI-Landschaft ist somit bemerkenswert. Während westliche Konzerne wie OpenAI seit Jahren dominieren, zeigt DeepSeek, dass Chinas KI-Industrie ernsthafte Konkurrenz darstellen kann. Das Vorantreiben spezialisierter Modelle wie Prover V2 im Bereich der mathematischen Beweisführung ergänzt die vielfältigen Anwendungen von KI, die von Sprache über Bildgenerierung bis hin zu wissenschaftlicher Forschung reichen. Zudem sorgt die Veröffentlichung solcher innovativer Modelle für frischen Wind in der Diskussion um die Zukunft von KI.
