Neben OpenAI und Google Deepmind hat auch das KI-Start-up Harmonic mit seinem Modell Aristotle bei der diesjährigen Internationalen Mathematik-Olympiade (IMO) 2025 eine Goldmedaillenleistung erzielt. Doch das Start-up verfolgt damit nicht AGI - sondern "mathematische Superintelligenz".
Laut Harmonic handelt es sich bei Aristotle um das erste KI-System, das sämtliche Lösungen formal verifiziert und damit ohne menschliche Prüfung auskommt. Die vollständigen Beweise wurden öffentlich auf Github veröffentlicht.
Im Gegensatz zu ähnlichen Erfolgen von Google Deepmind und OpenAI, deren Modelle die IMO-Aufgaben in natürlicher Sprache bearbeiteten, übersetzte Harmonic die Aufgaben in formale, maschinenlesbare Form und überprüfte die Lösungen mit dem Beweissystem Lean4. Die Beweisketten reichen dabei bis zu den mathematischen Axiomen zurück und bieten laut Unternehmen eine „maschinenprüfbare Garantie der Korrektheit“.
Verifikation statt Halluzination
Harmonic positioniert Aristotle als Antwort auf ein zentrales Problem moderner KI-Anwendungen: das sogenannte „Verification Problem“. In vielen technischen Bereichen – etwa der Softwareentwicklung – verbringen Menschen laut Harmonic zunehmend mehr Zeit mit der Überprüfung von KI-generierten Inhalten als mit deren Erstellung. Aristotle soll dies durch formale Verifikation vermeiden und damit eine neue Qualität von Vertrauenswürdigkeit erreichen.
Quelle: Harmonic
„Innerhalb der von Aristotle unterstützten quantitativen Domänen garantieren wir tatsächlich, dass es keine Halluzinationen gibt“, sagte Harmonic-CEO Tudor Achim gegenüber TechCrunch. Grundlage dafür ist die Ausgabe in der Programmiersprache Lean, die in sicherheitskritischen Bereichen wie Luftfahrt und Medizintechnik zur Verifikation eingesetzt wird.
Beta-App gestartet, API geplant
Parallel zur Ankündigung der IMO-Leistung hat Harmonic eine Beta-Version von Aristotle für iOS veröffentlicht. Die App zeigt bei komplexen mathematischen Fragen die Lösung und den zugehörigen Lean-Code. Zudem lassen sich Aufgaben per Foto erfassen und mehrere Probleme gleichzeitig lösen. Interessierte können sich auf aristotle.harmonic.fun für die Warteliste registrieren. Eine Android-Version ist ebenfalls verfügbar.
Laut Harmonic sind eine Web-App sowie eine API für Unternehmensanwendungen in Vorbereitung. Ziel ist es, Aristotle über den Bildungsbereich hinaus in alle mathematisch geprägten Disziplinen wie Physik, Statistik oder Informatik zu tragen.
