GDEPO: Neue Methode steigert Reinforcement-Learning beim automatischen Theorembeweis

In der Welt des automatischen Theorembeweisens (ATP) hat sich Reinforcement Learning als Schlüsseltechnologie etabliert. Der aktuelle Standard, der Group Relative Policy Optimization (GRPO) Algorithmus, stößt jedoch auf zwei gravierende Hindernisse: Erstens kann die Schätzung der relativen Belohnung bei zusammengesetzten Rewards im Widerspruch zur binären Rückmeldung des formalen Verifiers stehen. Zweitens führt die statische Stichprobenstrategie dazu, dass komplette Datenbatches verworfen werden, wenn keine gültige Beweisschrittfolge gefunden wird, was zu erheblichem Datenverlust führt.

Die neue Methode GDEPO – Group Dual-dynamic and Equal-right-advantage Policy Optimization – löst diese Probleme elegant. Sie kombiniert drei zentrale Mechanismen: Erstens wird bei ungültigen Batches dynamisch neu gesampelt, bis ein gültiger Beweis vorliegt. Zweitens trennt die „equal-right advantage“-Strategie das Vorzeichen der Vorteilfunktion (basierend auf Korrektheit) von ihrer Größe (moduliert durch Hilfsrewards), wodurch stabile und korrekte Policy-Updates gewährleistet werden. Drittens werden bei anfänglich fehlgeschlagenen, aber letztlich erfolgreichen Samples zusätzliche Gradientenschritte durchgeführt, um das Lernen bei schwierigen Fällen zu beschleunigen.

Experimentelle Ergebnisse auf drei unterschiedlichen Datensätzen – MinF2F-test, MathOlympiadBench und PutnamBench – belegen die Wirksamkeit von GDEPO. Die Ablationsstudien zeigen, dass jede der drei Kernkomponenten einen signifikanten Beitrag zur Leistungssteigerung leistet. Damit stellt GDEPO einen wichtigen Fortschritt dar, der die Effizienz und Zuverlässigkeit von Reinforcement-Learning-Ansätzen im automatischen Theorembeweis deutlich verbessert.