Mistral veröffentlicht Open-Source-Modell für formale Mathematik und Code-Verifikation

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.

Obwohl das Modell hauptsächlich für Mathematik trainiert wurde, zeigt es laut Mistral starke Fähigkeiten in der Code-Verifikation. In einem praktischen Test überprüfte es 57 Open-Source-Repositories und fand dabei fünf bisher unbekannte Fehler, darunter einen Overflow-Bug in der Rust-Bibliothek varinteger. Das Modell ist über Hugging Face und eine kostenlose API verfügbar. Das Training umfasste Mid-Training, überwachtes Feintuning und Reinforcement Learning.