de.wedoany.com-Bericht: Das europäische KI-Unternehmen Mistral AI hat am 2. dieses Monats (Ortszeit) das Modell Leanstral 1.5 für die formale Beweissprache Lean 4 vorgestellt. Das Modell verfügt über insgesamt 119B Parameter, aktiviert 6B Parameter und wird unter der Apache-2.0-Lizenz als Open Source veröffentlicht.

Mistral AI gibt an, dass Leanstral 1.5 im Validierungs- und Testsatz des formalen Mathematik-Benchmarks miniF2F eine Abschlussrate von 100 % erreicht hat; von den 672 Lean-4-Aufgaben im PutnamBench-Wettbewerbsaufgabensatz wurden 587 gelöst; bei der FATE-Reihe abstrakter Algebra-Benchmarks erreichte das Modell auf Master-Niveau (FATE-H) eine Erfolgsquote von 87 % und auf Doktor-Niveau (FATE-X) von 34 %, jeweils die beste Leistung. Diese Tests zeigen, dass die mathematischen Fähigkeiten des Modells ein brauchbares Niveau erreicht haben.

Mistral AI betont die Kostenvorteile des neuen Modells: Für Aufgaben aus dem PutnamBench-Datensatz betragen die durchschnittlichen Lösungskosten von Leanstral 1.5 nur 4 US-Dollar, während Seed-Prover 1.5 über 300 US-Dollar und Aleph Prover 54 bis 68 US-Dollar benötigt.

In realen Anwendungsszenarien markierte Leanstral 1.5 in 57 getesteten Codebasen 47 Verstöße, von denen 11 auf echte Fehler hinwiesen, darunter 5 Probleme, die zuvor nicht auf GitHub gemeldet worden waren.