Das chinesische KI-Unternehmen DeepSeek hat mit Prover V2 ein neues Open-Source-Sprachmodell zur Verifizierung mathematischer Beweise veröffentlicht. Das 671 Milliarden Parameter umfassende Modell ist unter der MIT-Lizenz auf Hugging Face verfügbar und basiert vermutlich auf DeepSeeks R1-Modell, welches zuvor für Aufsehen sorgte. Trotz der Quantisierung auf 8-Bit-Gleitkommagenauigkeit benötigt Prover V2 aufgrund seiner Größe erhebliche Hardware-Ressourcen.
Das chinesische KI-Unternehmen DeepSeek hat ein neues Open-Source-Sprachmodell namens Prover V2 vorgestellt, wie Cointelegraph berichtet. Das auf der Plattform Hugging Face gehostete Modell ist auf die Verifizierung mathematischer Beweise spezialisiert und steht unter der MIT-Lizenz.
Mit 671 Milliarden Parametern übertrifft Prover V2 seine Vorgänger Prover V1 und Prover V1.5, die im August 2024 veröffentlicht wurden, deutlich. Wie in einem Artikel zu Prover V1 erläutert, wurde das Modell darauf trainiert, mathematische Aufgaben mithilfe der Programmiersprache Lean 4 in formale Logik zu übersetzen. Lean 4 wird häufig für Theorembeweise eingesetzt. Laut den Entwicklern komprimiert Prover V2 mathematisches Wissen in ein Format, das die Generierung und Überprüfung von Beweisen erleichtert und somit Forschung und Lehre unterstützen kann.
Die Veröffentlichung der Modellgewichte ermöglicht die lokale Ausführung der KI ohne Abhängigkeit von externen Servern. Allerdings benötigen moderne Sprachmodelle leistungsfähige Hardware, da die hohe Parameteranzahl zu großen Dateien führt, die viel RAM oder VRAM (GPU-Speicher) und Rechenleistung beanspruchen. Prover V2 ist etwa 650 Gigabyte groß und soll im RAM oder VRAM ausgeführt werden. Um die Größe zu reduzieren, wurden die Gewichte von Prover V2 auf 8-Bit-Gleitkommagenauigkeit quantisiert, wodurch jeder Parameter nur die Hälfte des üblichen 16-Bit-Speicherplatzes benötigt.
Prover V1 basiert auf dem DeepSeekMath-Modell mit sieben Milliarden Parametern und wurde mit synthetisch generierten Daten feinabgestimmt. Synthetische Daten werden von KI-Modellen erzeugt und für das Training anderer KI-Modelle verwendet, da von Menschen generierte Daten als immer knapper werdende Ressource für qualitativ hochwertige Trainingsdaten gelten. Prover V1.5 verbesserte die vorherige Version durch Optimierungen bei Training und Ausführung und erreichte eine höhere Genauigkeit in Benchmarks. Die Verbesserungen von Prover V2 sind bisher unklar, da zum Zeitpunkt der Erstellung dieses Textes noch kein Forschungsbericht oder weitere Informationen veröffentlicht wurden.
Die Anzahl der Parameter in Prover V2 deutet darauf hin, dass es wahrscheinlich auf dem vorherigen R1-Modell des Unternehmens basiert. Bei seiner Veröffentlichung erregte R1 Aufsehen in der KI-Szene, da seine Leistung mit der des damaligen OpenAI-Modells vergleichbar war, wie Nature berichtet. Die Veröffentlichung von R1 als Open-Source-Modell wurde von einigen als Chinas "Sputnik-Moment" bezeichnet, wie Livescience berichtet, und löste Sicherheitsbedenken aus, da das Unternehmen Missbrauch nicht durch Einschränkungen bei Benutzeranfragen verhindern kann. Andererseits ermöglicht die öffentliche Freigabe der Gewichte den Zugang zu KI ohne Abhängigkeit von der Infrastruktur privater Unternehmen. DeepSeek folgt damit Metas Veröffentlichung der Open-Source-KI-Modelle der LLaMA-Serie, was zeigt, dass Open-Source-KI eine ernstzunehmende Konkurrenz zu OpenAIs Closed-Source-KI darstellt, so Cointelegraph.
Die Zugänglichkeit von Sprachmodellen hat sich durch Modelldestillation und Quantisierung verbessert. Bei der Destillation wird ein kompaktes "Schüler"-Netzwerk trainiert, das Verhalten eines größeren "Lehrer"-Modells zu imitieren, wodurch die Leistung bei gleichzeitiger Reduzierung der Parameter erhalten bleibt. Quantisierung reduziert die numerische Präzision der Modellgewichte, um die Größe zu verringern und die Inferenzgeschwindigkeit zu erhöhen. DeepSeeks R1 wurde in Versionen mit neu trainierten LLaMA- und Qwen-Modellen destilliert, die von 70 Milliarden bis zu 1,5 Milliarden Parametern reichen. Das kleinste dieser Modelle kann sogar zuverlässig auf einigen Mobilgeräten ausgeführt werden, wie Cointelegraph berichtet. DeepSeek arbeitet Berichten zufolge bereits an einem Nachfolger für R1, dem R2-Modell, das im April vorgestellt werden soll, wie NDTV berichtet.
Quellen:
