Neue Methode kombiniert Text- und Strukturinfos zur Premise-Auswahl in Lean

In der Welt der formalen Beweisführung stellt die Auswahl der richtigen Prämissen einen entscheidenden Engpass dar. Ein neues Verfahren aus dem arXiv-Preprint 2510.23637v1 löst dieses Problem, indem es Text- und Strukturinformationen miteinander verknüpft.

Die Autoren nutzen dichte Text-Embeddings der Lean-Formalismen und kombinieren diese mit Graph-Neuronalen Netzen, die über ein heterogenes Abhängigkeitsgraphen-Netzwerk laufen. Dieser Graph erfasst sowohl Zustands-Prämissen- als auch Prämissen-Prämissen-Beziehungen und ermöglicht so ein umfassenderes Verständnis der Zusammenhänge.

Auf dem LeanDojo Benchmark übertrifft die neue Methode das bisherige sprachbasierte ReProver-Baseline um mehr als 25 % bei allen üblichen Retrieval-Metriken. Diese beeindruckende Steigerung unterstreicht die Bedeutung relationaler Informationen für eine effektivere Prämissenwahl.

Die Ergebnisse zeigen deutlich, dass die Integration von strukturellen Abhängigkeiten die Leistungsfähigkeit von Theorem-Prover-Systemen erheblich steigern kann und eröffnen neue Perspektiven für die Skalierung großer formaler Bibliotheken.