Stell dir vor, eine KI könnte mathematische Beweise so einfach lösen, wie du ein Puzzle zusammensetzt. Forschende haben eine neue Methode entwickelt, die das möglich macht.
Stell dir vor, du musst ein schwieriges Mathe-Rätsel lösen. Du hast zwei Freunde, die dir helfen können. Der erste Freund kann dir Schritt für Schritt sagen, was du tun musst. Der zweite Freund kann dir direkt die Lösung zeigen. Beide Freunde sind sehr klug, aber sie arbeiten auf unterschiedliche Weise. Forschende haben eine neue Methode entwickelt, die beide Freunde zusammenbringt, um noch besser zu arbeiten. Diese Methode heißt HybridProver.
Was die Forschenden herausgefunden haben
Die Forschenden haben herausgefunden, dass HybridProver sehr gut funktioniert. Sie haben es mit einem schwierigen Datensatz getestet und eine Erfolgsquote von 59,4 Prozent erreicht. Das ist besser als alles, was vorher gemacht wurde. Sie haben auch festgestellt, dass die Qualität der Daten und die Art, wie die KI trainiert wird, sehr wichtig sind.
Wie haben sie das gemacht?
HybridProver arbeitet in zwei Schritten. Zuerst versucht es, den gesamten Beweis auf einmal zu finden. Dann nimmt es diesen Beweis und verbessert ihn Schritt für Schritt. Dazu nutzt es eine Kombination aus automatischen Werkzeugen und einer speziellen Art von KI, die große Mengen an Text verstehen kann. Die Forschenden haben HybridProver für ein spezielles Programm namens Isabelle entwickelt und es mit vielen Beispielen trainiert.
Warum ist das wichtig?
Diese Methode ist wichtig, weil sie hilft, komplexe Systeme zu überprüfen. Zum Beispiel können Flugzeuge oder Autos sicherer gemacht werden, wenn man sicher ist, dass ihre Software keine Fehler hat. HybridProver kann dabei helfen, diese Fehler zu finden und zu beheben.
Du willst mehr über die Studie wissen?
Die Forschenden hinter HybridProver sind Jilin Hu, Jianyu Zhang, Yongwang Zhao und Talia Ringer. Ihr Artikel „HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement“ wurde 2025 veröffentlicht.