Wir reden hier über zwei sehr unterschiedliche Arten von System.
AlphaProof und seine Nachfolger (Deepseek Prover, Aleph Prover usw.) sind spezialisierte Systeme und architektonisch nahe mit AlphaGo verwandt: Du hast einen formal eingegrenzten Zustandsraum (Brettpositionen, proof state), über dem du gewisse Aktionen (Zug, tactic) durchführen kannst. Dann kombiniert man neuronale Netze für Policy (nächster Zug?) und Value (Gewinnwahrscheinlichkeit?) mit klassischen Suchalgorithmen (MCTS).
AlphaGo Zero hat Policy- und Value-Network from scratch über Self-Play und Reinforcement Learning trainiert. Theorem-Prover benutzen vortrainierte LLMs als Backbone. Die grundsätzliche Methode ist relativ ähnlich.
Diese Systeme haben den großen Vorteil, dass du einen deterministischen Lean-Kernel zur Verifikation nutzen kannst. Ein weiterer Vorteil ist, dass du im Gegensatz zu reinen LLMs effektiver off-policy erkunden kannst: Du entdeckst bei der Suche Lösungswege, die das LLM allein nicht gefunden hätte. Dadurch outperformen solche Systeme reine LLMs in formalisierten Settings, aber der Compute-Overhead für die Suche ist hoch: Es ist viel teurer mit so einem System ein Problem zu lösen als mit einem reinen LLM.
Dazu kommt: Während AlphaGo Zero sein Policy- und Value-Network durch reines Self-Play und RL bootstrappen konnte, sind solche Theorem-Prover viel stärker durch ihren Policy-Prior constrained: Ihre Leistungsfähigkeit skaliert ganz wesentlich mit der Leistungsfähigkeit des LLM-Backbones.
Allein die Möglichkeit der formalen Verifizierung macht solche Systeme sehr wertvoll, aber ihre Entwicklung hängt letztlich von der Entwicklung der zugrundeliegenden LLMs ab.
Meine Bemerkung oben war tatsächlich auf reine LLMs (mit CoT/Reasoning) bezogen, mit denen ich einiges an Erfahrung (vs. null mit spezialisierten Provern/Lean) im Lösen mathematischer Probleme habe. Der Fortschritt, den die Models hier in den letzten ein, zwei Jahren gemacht haben, ist ähnlich spektakulär wie beim Coden.
Mal als Referenz in Bezug auf AlphaProof: Ein Jahr später war quasi jedes SOTA LLM in einem guten Agent-Harness in der Lage IMO-Gold-Level zu erreichen:
The International Mathematical Olympiad (IMO) is widely regarded as the world championship of high-school mathematics. IMO problems are renowned for their difficulty and novelty, demanding deep insight, creativity, and rigor. Although large language models perform well on many mathematical...
arxiv.org
Die neuesten Modelle sind nochmal spürbar besser geworden und bringen echten Mehrwert als Research-Assistenten - wenn auch noch nicht auf PhD-Level, wie öfter behauptet wird. Ich selbst setze hauptsächlich GPT 5.2 ein und würde mit hoher Konfidenz behaupten, dass es in allgemeiner mathematischer Problemlösekompetenz deutlich über einem durchschnittlichen Mathematik-Absolventen (Bachelor/Master) liegt.
Etwas ernüchtert musste ich z.B. neulich feststellen, dass es als erstes Model das Hauptresultat meiner Bachelorarbeit mühelos in vollständiger und rigoroser Form beweisen konnte. Geminis Kommentar in seiner Rolle als Juror, nachdem sein eigener Beweisversuch eher mittelmäßig ausgefallen war:
Ich gebe dem Beweis eine glatte 10 von 10 Punkten.
Der Beweis ist meinem in puncto mathematischer Strenge (Rigorosität), Detailtiefe und didaktischem Aufbau deutlich überlegen. Er liest sich wie ein hervorragend ausgearbeiteter Beweis aus einem fortgeschrittenen Lehrbuch zur Wahrscheinlichkeitstheorie.
(Mein eigener Beweis von damals hat es leider nur auf 7 von 10 Punkten gebracht.
)
