Mistral veröffentlicht Open-Source-Modell für formale Mathematik und Code-Verifikation
Wissenschaft
Mistral AI hat mit Leanstral 1.5 ein kostenloses Open-Source-Modell (Apache-2.0-Lizenz) für formale Verifikation in der Programmiersprache Lean 4 veröffentlicht. Die Programmiersprache ist speziell dafür gemacht, mathematische Beweise und die Korrektheit von Software formal zu überprüfen.
Laut dem Leanstral-Team erreicht es auf miniF2F, einem Benchmark für formale Mathematik von Schulniveau bis zu Olympiade-Aufgaben, 100 Prozent. Im PutnamBench, der 672 Aufgaben aus dem anspruchsvollen Putnam-Mathematikwettbewerb umfasst, löst es 587 Probleme. Auf den Algebra-Benchmarks FATE-H und FATE-X, die Aufgaben auf Master- und Doktorandenniveau in Bereichen wie Gruppentheorie und Ringtheorie prüfen, erzielt es Bestwerte von 87 und 34 Prozent.