SorryDB: KI-Prover testen echte Lean-Theoreme – neue dynamische Benchmark

Auf der Plattform arXiv wurde die neue Studie „SorryDB“ vorgestellt, die ein ständig aktualisiertes Benchmark für offene Lean-Aufgaben bereitstellt. Die Aufgaben stammen aus 78 realen Formalisierungsprojekten auf GitHub und ersetzen damit die bisher üblichen statischen Tests, die oft aus Wettbewerbsproblemen bestehen.

Durch die kontinuierliche Aktualisierung der Aufgaben verhindert SorryDB das Phänomen der Test‑Set‑Kontamination und liefert ein robustes Messinstrument dafür, wie gut ein KI-Agent neue formale Mathematikprojekte unterstützen kann. Gleichzeitig fördert die dynamische Natur der Benchmark die Entwicklung von Werkzeugen, die besser auf die Bedürfnisse der mathematischen Community abgestimmt sind und komplexe Abhängigkeiten besser verstehen.

In der Evaluation wurden verschiedene Ansätze getestet – von generellen großen Sprachmodellen über agentische Systeme bis hin zu spezialisierten symbolischen Beweiser. Für einen ausgewählten Snapshot von 1.000 Aufgaben zeigte sich, dass die agentische Methode auf Basis von Gemini Flash die höchste Leistung erzielte. Dennoch übertrifft sie nicht eindeutig andere verfügbare LLMs, spezialisierte Beweiser oder sogar eine kuratierte Liste von Lean‑Taktiken, was die Komplementarität der unterschiedlichen Ansätze unterstreicht.