Ein In-Context Learning Agent für formales Beweisführen

Wir stellen einen in-Context-Lern-Agenten für die formale Beweisführung in Umgebungen wie Lean und Coq vor. Derzeitige state-of-the-art-Modelle für dieses Problem werden auf umgebungsspezifische Beweisdaten fine-tuned. Im Gegensatz dazu verwendet unser Ansatz, COPRA genannt, wiederholt ein leistungsstarkes, allgemein einsetzbares Großmodell (GPT-4), um innerhalb eines zustandsbehafteten Rückverfolgungs-Suchverfahrens Beweisschritte (Tactics) vorzuschlagen. Vorgeschlagene Tactics werden in der zugrundeliegenden Beweisumgebung ausgeführt. Das Feedback aus der Ausführung dient dazu, den Prompt für die nächste Modellabfrage zu erstellen, zusammen mit ausgewählten Informationen aus der Suchhistorie und Lemmata, die aus einer externen Datenbank abgerufen wurden. Wir evaluieren unsere Implementierung von COPRA auf dem miniF2F-Benchmark für Lean sowie auf einer Reihe von Coq-Aufgaben aus dem CompCert-Projekt. Auf diesen Benchmarks übertrifft COPRA die Few-Shot-Aufrufe von GPT-4 deutlich. Zudem schneidet es gegenüber auf Fine-Tuning basierenden Ansätzen gut ab und erreicht eine bessere Leistung als ReProver, ein state-of-the-art-Fine-Tuning-Ansatz für Lean, hinsichtlich der Pass@1-Metrik. Unser Code und die verwendeten Daten sind unter https://github.com/trishullab/copra verfügbar.