IndiMathBench: Verifizierte Benchmark für automatisierte Mathematikformalisierung

IndiMathBench ist ein neu entwickeltes, von Menschen verifiziertes Benchmark‑Set, das die Leistungsfähigkeit von automatischen Theorem‑Provern testen soll. Das Set besteht aus 312 formalen Lean‑4‑Theoremen, die jeweils mit einer informellen Aufgabenstellung aus den Indian Mathematics Olympiads verknüpft sind.

Die Formalisierung erfolgt über einen KI‑gestützten, menschlich unterstützten Pipeline‑Ansatz. Dabei werden Aufgaben zunächst nach Kategorien abgefragt, anschließend durch wiederholtes Compiler‑Feedback verfeinert und schließlich mit Ensemble‑Modellen optimiert. Die daraus resultierenden Kandidaten werden von Experten über ein interaktives Dashboard geprüft, das automatisch Qualitätszusammenfassungen liefert.

Tests mit aktuellen Spitzenmodellen zeigen, dass die automatische Formalisierung noch immer große Herausforderungen birgt: Es bestehen erhebliche Lücken zwischen syntaktisch korrekten und semantisch richtigen Formulierungen, und die Erfolgsraten beim Theorem‑Proving bleiben trotz iterativer Verbesserungen niedrig. IndiMathBench stellt damit ein anspruchsvolles Testfeld für zukünftige Fortschritte in der mathematischen KI‑Verarbeitung dar. Das Projekt ist unter https://github.com/prmbiy/IndiMathBench verfügbar.