Lyra: Die Orchestrierung der dualen Korrektur im automatisierten Beweisen von Sätzen

Große Sprachmodelle (LLMs) eröffnen ein vielversprechendes Forschungsfeld im Bereich des formalen Beweisens. Dennoch bleibt ihr volles Potenzial – insbesondere hinsichtlich der Reduktion von Halluzinationen und der Verbesserung durch Rückmeldungen von Beweisverfahren (Prover-Error-Meldungen) – bisher weitgehend unerforscht. Um die Wirksamkeit von LLMs in diesem Bereich zu steigern, stellen wir Lyra vor, einen neuen Rahmen, der zwei unterschiedliche Korrekturmechanismen einsetzt: Tool-Korrektur (TC) und Vermutungs-Korrektur (CC). Zur Implementierung der Tool-Korrektur im Nachbearbeitungsschritt formaler Beweise nutzen wir vorheriges Wissen, um vordefinierte Beweiswerkzeuge (z. B. Sledgehammer) einzusetzen, um falsche Werkzeuge gezielt zu ersetzen. Die Tool-Korrektur trägt erheblich zur Minderung von Halluzinationen bei und verbessert somit die Gesamtgenauigkeit des Beweises. Zusätzlich führen wir die Vermutungs-Korrektur ein, einen Fehlerfeedback-Mechanismus, der interaktiv mit dem Beweisverfahren arbeitet, um formale Beweisvermutungen mithilfe von Beweisverfahrensfehlermeldungen zu verfeinern. Im Gegensatz zu früheren Verfeinerungsrahmen verfeinert unsere Methode die Generierung mittels Anweisungen, ohne jedoch Paare aus (Generierung, Fehler & Verfeinerung) zu sammeln. Unser Ansatz erreicht state-of-the-art (SOTA)-Leistung sowohl auf dem miniF2F-Validierungssatz (48,0 % → 55,3 %) als auch auf dem Testset (45,5 % → 51,2 %). Zudem präsentieren wir drei Aufgaben aus der Internationalen Mathematikolympiade (IMO), die von Lyra gelöst wurden. Wir sind überzeugt, dass die Tool-Korrektur (Nachbearbeitung zur Minderung von Halluzinationen) und die Vermutungs-Korrektur (Subgoal-Anpassung durch Interaktion mit der Umgebung) vielversprechende Wege für zukünftige Forschung in diesem Bereich darstellen.