KI lernt, Gegenbeispiele zu finden: LLMs erzeugen formale Gegenbeweise

Mathematisches Denken erfordert zwei zentrale Fähigkeiten: das Erstellen rigoroser Beweise für wahre Aussagen und das Aufspüren von Gegenbeispielen, die falsche Behauptungen widerlegen. Bisher konzentrieren sich KI‑Projekte im mathematischen Bereich fast ausschließlich auf die Beweisführung, während die Suche nach Gegenbeispielen vernachlässigt wird. In der vorliegenden Arbeit wird dieses Defizit behoben, indem große Sprachmodelle (LLMs) gezielt darauf trainiert werden, Gegenbeispiele zu generieren und gleichzeitig formale Beweise zu liefern, die automatisch im Lean‑4 Theoremprover überprüft werden können.

Um die Lernfähigkeit der Modelle zu steigern, wird eine symbolische Mutationsstrategie eingesetzt. Diese Technik erzeugt vielfältige Trainingsdaten, indem Theoreme systematisch extrahiert und ausgewählte Hypothesen entfernt werden. Durch die Kombination dieser synthetisierten Beispiele mit sorgfältig kuratierten Datensätzen entsteht ein Multi‑Reward‑Expert‑Iteration‑Framework, das die Effektivität und Effizienz des Trainings von LLMs für Gegenbeispiel‑Generierung und Theoremproving deutlich verbessert.

Die Experimente, die auf drei neu zusammengestellten Benchmarks basieren, zeigen die Vorteile des Ansatzes eindeutig. Sowohl die Mutationsstrategie als auch das Trainingsframework führen zu signifikanten Leistungssteigerungen, was die Rolle von KI im mathematischen Beweis‑ und Gegenbeweis‑Prozess weiter voranbringt.