Mistral lanciert KI für mathematische Codeprüfung

(Source: horizon / stock.adobe.com)

(Source: horizon / stock.adobe.com)

Das französische KI-Start-up Mistral AI erweitert sein Angebot um ein KI-Modell für die mathematische Überprüfung von Software. Mit Leanstral 1.5 veröffentlicht das Unternehmen ein frei verfügbares Sprachmodell und stellt dessen Quellcode sowie die Modellgewichte unter der Apache-2.0-Lizenz bereit. 

Das Modell erstellt und überprüft mathematische Beweise mit Lean 4, einer Programmiersprache und Beweisumgebung, mit der sich mathematische Aussagen Schritt für Schritt formal beschreiben und überprüfen lassen. Anders als klassische Testverfahren, die nur ausgewählte Eingaben prüfen, soll die sogenannte formale Verifikation mathematisch nachweisen, dass ein Programm bestimmte Eigenschaften in allen zulässigen Fällen erfüllt, wie Mistral AI mitteilt.

Bestwerte bei mathematischen Beweisen

Nach Angaben von Mistral erreicht Leanstral 1.5 auf mehreren etablierten Benchmarks für automatisierte mathematische Beweisführung neue Höchstwerte. So löst das Modell sämtliche Aufgaben des "miniF2F"-Benchmarks und 587 von 672 Aufgaben des "PutnamBench", der auf Problemen des renommierten Mathematikwettbewerbs Putnam basiert. Auch auf den Algebra-Benchmarks "FATE-H" und "FATE-X" erzielt das Modell laut Hersteller neue Bestwerte.

Laut Mistral erzielt Leanstral 1.5 auf mehreren Benchmarks für mathematische Beweisführung Bestwerte und schneidet auf PutnamBench nur knapp schlechter ab als Aleph Prover. (Source: Mistral AI)

Über Mathematik hinaus sieht Mistral konkrete Einsatzmöglichkeiten in der Softwareentwicklung. Das Modell soll Programmcode auf seine Korrektheit prüfen und dabei Fehler aufdecken, die mit klassischen Testverfahren nur schwer zu finden sind. Gemäss Mitteilung untersuchte Leanstral 57 Open-Source-Projekte und entdeckte dabei fünf bislang unbekannte Softwarefehler. Diese Resultate stammen allerdings ausschliesslich von Mistral und wurden bislang nicht unabhängig bestätigt.

KI arbeitet wie ein Softwareentwickler

Das Modell agiert laut Mistral als sogenannter agentischer Assistent. Es erstellt nicht nur mathematische Beweise, sondern bearbeitet Dateien, wertet Compiler-Rückmeldungen aus und verbessert seine Lösungsansätze schrittweise. Mistral trainierte Leanstral 1.5 unter anderem mit Reinforcement Learning - einer Methode, bei der ein KI-Modell durch Belohnungen lernt, erfolgreiche Strategien zu entwickeln.

Die mathematische Überprüfung von Programmcode galt lange als Nischenwerkzeug für besonders sicherheitskritische Anwendungen. Mit spezialisierten KI-Modellen wollen Unternehmen wie Mistral diesen aufwendigen Prozess nach eigenen Angaben vereinfachen und mehr Entwicklerinnen und Entwicklern zugänglich machen.

Übrigens: Open-Source-KI gewinnt auch in der Schweiz an Bedeutung. Wie Forschende und Unternehmen auf offene Sprachmodelle setzen und wie fast jede und jeder zu einer eigenen KI kommt, erfahren Sie im Bericht zur diesjährigen Open Source AI Conference.