Gerade wurde Gemini 4 Carbon weltweit vollständig freigegeben, und die innerhalb von 4 Wochen erstellten 6,5 Millionen Zeilen mathematischer Beweise bestätigen die Sicherheit von Signal.

Gerade hat Google DeepMind die offizielle Freigabe von Gemini 4 Carbon heute bekanntgegeben, das als „das derzeit leistungsstärkste Modell von Google“ bezeichnet wird, speziell für komplexe, lang andauernde Aufgaben ausgelegt ist, mehr Inferenzressourcen einsetzen kann, um Probleme eingehend zu erforschen, und durch fortlaufende Ausführung, Überprüfung und Korrektur komplexe Aufgaben in Software-Engineering, Cybersicherheit, Wissensarbeit und wissenschaftlicher Forschung abschließen kann.

Im Vergleich zum früheren Gemini 4 Argon ist die Positionierung von Carbon klarer definiert: Es begnügt sich nicht damit, schnell eine Antwort zu geben, sondern ist bereit, mehr Zeit und Rechenressourcen aufzuwenden, um eine komplexe Angelegenheit wirklich abzuschließen.

Demis Hassabis hat ein anschauliches Beispiel gegeben: „Carbon hat das Binärformat des ursprünglich von mir entwickelten Spiels «Theme Park» rückentwickelt, eine neue auf DeepMind bezogene Freizeiteinrichtung in das Spiel hinzugefügt und das gesamte Spiel in einem Zug auf die Web-Plattform portiert.“

Darunter hat er zudem ein Vergleichsvideo angefügt, das im gleichen Zeitraum letzten Jahres mit Gemini 3 erstellt wurde, und äußerte sich beeindruckt: „In weniger als einem Jahr hat sich Gemini von Version 3 zu Version 4 weiterentwickelt, der Fortschritt ist wirklich erstaunlich……

Es ist wirklich unglaublich, all das mit eigenen Augen zu sehen!“

Diese leistungsstarke Fähigkeit steht jetzt allen Nutzern weltweit zur Verfügung! Laut offiziellen Angaben wird Gemini 4 Carbon ab sofort über folgende Kanäle freigegeben:

• Verbraucher: Abonnenten von Google AI Ultra können es über die Gemini-App und den KI-Modus in der Google-Suche nutzen.
• Entwickler und Unternehmen: Sie können über die APIs in Google AI Studio und Android Studio entwickeln; Abonnenten von Google AI Ultra können es zudem über Google Antigravity nutzen, Unternehmenskunden über Gemini for Business.
• Wissenschaftler und Forscher: Sie können über Google Antigravity einen Antrag stellen und erhalten ggf. eine kostenlose Nutzungsberechtigung für 6 Monate.
• Cybersicherheitsverteidiger: Sie können beantragen, am Fairwind-Programm teilzunehmen, um die Nutzungsberechtigung von Carbon im Bereich der Cybersicherheit zu erhalten.

Um die Fähigkeit von Gemini 4 Carbon zur Bearbeitung komplexer Aufgaben in der wissenschaftlichen Forschung zu demonstrieren, hat Google DeepMind unmittelbar nach der offiziellen Veröffentlichung des Modells ein repräsentatives Beispiel vorgelegt und eine Studie namens AlphaProof Code veröffentlicht: Die Forscher nutzten einen KI-Agenten, der von Gemini 4 Carbon angetrieben wird, um eine formale Verifikation des zugrundeliegenden Codes des Signal-Verschlüsselungsprotokolls durchzuführen, und erzeugten schließlich mehr als 6,5 Millionen Zeilen maschinengeprüfter mathematischer Beweiscodes.

Diese Arbeit, die normalerweise ein Expertenteam mehrere Jahre in Anspruch nehmen würde, wurde schließlich in nur vier Wochen abgeschlossen.

Noch wichtiger ist, dass dies bedeutet, dass KI den Schritt von „Code schreiben“ zu „mathematisch beweisen, dass Code sicher ist“ vollzieht.

Von der lang andauernden Inferenz zur tatsächlichen Erledigung komplexer Arbeiten

Google positioniert Gemini 4 Carbon als das derzeit am besten geeignete Modell zur Bearbeitung schwieriger, mehrstufiger Aufgaben.

Im Software-Engineering kann es komplexe Codebasen bewältigen, modulübergreifende Problemdiagnosen, Architekturanpassungen und mehrstufige Debugging-Arbeiten durchführen; in der wissenschaftlichen Forschung kann es kontinuierlich Hypothesen zu offenen Problemen erforschen, Beweise analysieren und Ergebnisse verifizieren; in der Wissensarbeit kann es zudem eine große Menge komplexer Dokumente, Daten und strukturierter Informationen verarbeiten.

Dahinter steckt ein wichtiges Design: Extended Verification Loops (Erweiterte Überprüfungsschleifen).

Bei komplexen Aufgaben setzt Carbon mehr Thinking Tokens ein, erforscht verschiedene Lösungswege und überprüft die Ergebnisse während der Ausführung wiederholt. Wenn es Probleme erkennt, kann es weiterhin Änderungen vornehmen und Tests durchführen, bis es ein zuverlässigeres Ergebnis erzielt.

In den von Google veröffentlichten unabhängigen Workflow-Benchmark-Tests belegte Carbon den ersten Platz bei CursorBench 4.0, Perplexity WANDR und Zapier AutomationBench. Google gab zudem an, dass die Kosten pro einzelner Aufgabe in diesen Tests mehr als doppelt niedriger liegen als bei dem nächsten externen Modell mit der besten Leistung.

Gleichzeitig stellt Google derzeit die Funktion /swarm in Google Antigravity in der Vorschau vor: Nutzer müssen nur eine Aufgabe angeben, damit mehrere Agenten ein kooperatives Team bilden, das jeweils Aufgaben wie Architekturdesign, Aufgabenkoordination, Code-Implementierung und Überprüfung übernimmt.

Carbon kann für die Abschnitte zuständig sein, die die tiefste Inferenz erfordern, während andere leichtere Modelle spezifische Aufgaben parallel bearbeiten.

Von der Modellfähigkeit bis zur Zusammenarbeit mehrerer Agenten möchte Google erreichen, dass die von KI übernommenen Arbeiten komplexer werden und dem echten professionellen Arbeitsablauf näher kommen.

6,5 Millionen Zeilen mathematischer Beweis: Ein KI-Agent hat eine „Sicherheitsuntersuchung“ für Signal durchgeführt

Wenn Gemini 4 Carbon die Obergrenze seiner Fähigkeiten demonstriert, ist AlphaProof Code eine sehr konkrete Fähigkeitsverifikation.

Diese Studie zielt auf ein seit langem bestehendes Problem im Bereich der Softwaresicherheit ab: Wie kann man beweisen, dass eine tatsächlich ausgeführte Software die vom Entwickler geforderten Sicherheitseigenschaften erfüllt?

Nehmen wir Signal als Beispiel.

Als weit verbreitetes Verschlüsselungskommunikationsprotokoll basiert die Sicherheit von Signal auf einer Reihe komplexer kryptografischer Mechanismen. In der Vergangenheit konnten Kryptografieexperten auf mathematischer Ebene analysieren, ob das Protokolldesign sicher ist, und auch durch Code-Überprüfungen und Tests nach Schwachstellen suchen.

Hier besteht jedoch immer eine Lücke: Ein theoretisch sicheres Protokoll bedeutet nicht, dass der Code, der letztendlich auf den Geräten der Nutzer ausgeführt wird, zwangsläufig sicher ist.

Vom Protokolldesign bis zur tatsächlichen Ausführung durchläuft der Code noch Implementierung, Kompilierung und Optimierung. Ein winziger Implementierungsfehler kann dazu führen, dass das ursprünglich strenge Sicherheitsdesign unwirksam wird.

Die traditionelle Formale Verifikation (Formal Verification) versucht, dieses Problem mit mathematischen Beweisen zu lösen: Die Sicherheitsbedingungen, die die Software erfüllen muss, werden in strenge mathematische Aussagen umgewandelt, und dann wird bewiesen, dass der tatsächliche Code diese Bedingungen erfüllt.

Das Problem besteht darin, dass diese Arbeit extrem komplex ist und Experten oft viel Zeit in Anspruch nehmen müssen.

Das von Google DeepMind diesmal vorgestellte AlphaProof Code möchte diese Hürde mithilfe von KI-Agenten senken.

Das Forschungsteam hat zuerst zusammen mit dem Modell die Sicherheitsziele von Signal in mathematische Spezifikationen umgewandelt, die von der Lean-Sprache verstanden werden können, und diese von menschlichen Experten einzeln prüfen lassen. Anschließend begannen mehrere von Gemini 4 Carbon angetriebene Agenten, automatisch Beweise zu konstruieren, um zu beweisen, dass der tatsächliche Code diese Sicherheitsanforderungen erfüllt.

Der entscheidende Punkt hierbei ist, dass die Forschung nicht auf der Ebene des Protokolldesigns oder des Quellcodes stehen geblieben ist, sondern weiter bis zum endgültig kompilierten Gerätecode vorgedrungen ist.

Die Forscher haben die formale Semantik des AArch64-Befehlssatzes erstellt und den kompilierten Maschinencode in den Verifikationsbereich einbezogen. Das bedeutet, dass sie versucht haben, den Code zu beweisen, der tatsächlich auf dem Gerät ausgeführt wird, und nicht nur die theoretische Algorithmusbeschreibung.

Schließlich hat AlphaProof Code etwa 6,5 Millionen Zeilen Lean-Beweiscodes für die Kernimplementierung von Signal erzeugt, die auf etwa 26.000 Zeilen geprüfter formaler Spezifikationen und Maschinencodesemantik basieren.

Der gesamte Verifikationsprozess dauerte nur vier Wochen. Die KI-Agenten markieren zudem automatisch die Teile, die einer weiteren Überprüfung durch Menschen bedürfen, sodass letztendlich nur etwa 1 % der Codebasis zusätzliche menschliche Aufmerksamkeit erfordert, während alle übrigen Beweise von dem vertrauenswürdigen Kernel von Lean maschinell überprüft werden.

Noch wichtiger ist, dass dieses System nicht nur Beweise für korrekten Code erzeugt.

Das Forschungsteam hat absichtlich zwei Schwachstellen, die in der Vergangenheit tatsächlich existierten und später behoben wurden, wieder in eine isolierte Version des Signal-Codes eingefügt. Infolgedessen hat AlphaProof Code erfolgreich Gegenbeweise erzeugt, die maschinell überprüft wurden, und erkannt, dass diese Codes die ursprünglichen Sicherheitsanforderungen nicht erfüllen.

Dies zeigt, dass es nicht nur bei der Verifikation korrekter Implementierungen helfen kann, sondern auch die Fähigkeit besitzt, bestimmte fehlerhafte Implementierungen zu erkennen.

Der nächste Schritt der KI-Programmierung: Den Code vertrauenswürdig machen?

Die Bedeutung dieser Studie geht weit über die Durchführung einer Sicherheitsverifikation für Signal hinaus.

In der Vergangenheit war die Formale Verifikation eines der teuersten Sicherheitsmaßnahmen im Software-Engineering. Selbst für sehr wichtige Systeme benötigt ein Expertenteam oft mehrere Jahre, um zu beweisen, dass ihr Code strenge Sicherheitseigenschaften erfüllt.

Jetzt übernehmen KI-Agenten einen Großteil der anstrengenden Arbeiten: Formale Spezifikationen schreiben, Beweiswege erforschen, Lean-Code generieren, der dann von einem unabhängigen Beweiskernel überprüft wird.

Natürlich bedeutet dies nicht, dass KI bereits in der Lage ist, unabhängig zu beweisen, dass jede Software absolut sicher ist. Menschliche Experten müssen weiterhin die Sicherheitspezifikationen definieren und prüfen, und das Beweissystem kann nur garantieren, dass der Code die ausdrücklich formulierten Eigenschaften erfüllt.

Aber dieser Weg zeigt bereits eine neue Möglichkeit auf: Wenn Agenten kontinuierlich schlussfolgern, Tools aufrufen, komplexe Zwischenergebnisse konstruieren und durch externe Verifikationsmechanismen wiederholt überprüfen können, hat KI die Chance, Arbeiten zu übernehmen, die früher von Expertenteams über lange Zeit erledigt werden mussten.

Google DeepMind hat zudem angegeben, dass diese Technologie in Zukunft auf kritische Infrastrukturen wie Firmware von medizinischen Geräten und Software für Stromnetze ausgeweitet werden soll, und in Kombination mit dem automatischen Schwachstellenbehebungs-Tool CodeMender einen vollständigeren Sicherheitskreislauf für Software bilden soll – von der Erkennung von Schwachstellen über die Behebung von Problemen bis zur formalen Verifikation.

Von der Veröffentlichung von Gemini 4 Carbon bis zur Verifikation von Signal durch AlphaProof Code zeigt Google dieselbe Richtung: Der Wert von Modellen erstreckt sich zunehmend von der Beantwortung von Fragen hin zur Übernahme komplexer Arbeiten.

Und wenn KI nicht nur Code schreiben, sondern Menschen dabei helfen kann, mathematisch zu beweisen, dass der Code die Sicherheitsanforderungen erfüllt, wird die Grenze der Fähigkeiten von Agenten in ein neues Gebiet verschoben.

Und Sie? Wie sehen Sie es, dass heutige große Modelle nicht mehr nur darauf abzielen, Ranglisten zu gewinnen, sondern komplexere mathematische und kryptografische Probleme zu erforschen? Hinterlassen Sie gerne einen Kommentar zum Austausch!

Referenzlinks:

https://x.com/GoogleDeepMind/status/2120219371473617099

https://blog.google/innovation-and-ai/models-and-research/gemini-models/gemini-4-carbon-now-available/?utm_source=x&utm_medium=social&utm_campaign=&utm_content=

https://x.com/sundarpichai/status/2120207062655549933

https://deepmind.google/blog/introducing-alphaproof-code/

Dieser Artikel stammt aus dem WeChat-Offiziellen Konto „Jiqi Zhixin“ (ID: almosthuman2014), Autor: Mitarbeiter im Bereich KI, veröffentlicht mit Genehmigung von 36Kr.