Lösen von Ungleichheitsbeweisen mit großen Sprachmodellen

Zusammenfassung

Die Beweisung von Ungleichungen, die in verschiedenen wissenschaftlichen und mathematischen Bereichen von entscheidender Bedeutung ist, testet fortgeschrittene Denkfähigkeiten wie das Entdecken enger Schranken und die strategische Anwendung von Theoremen. Dies macht sie zu einer eigenständigen, anspruchsvollen Herausforderung für große Sprachmodelle (LLMs), die über allgemeines mathematisches Problemlösen hinausgeht. Der Fortschritt in diesem Bereich wird durch bestehende Datensätze behindert, die oft knapp, synthetisch oder streng formal sind. Wir adressieren dies, indem wir eine informelle, aber überprüfbare Aufgabenformulierung vorschlagen, die die Beweisung von Ungleichungen in zwei automatisch überprüfbare Teilaufgaben umwandelt: Schätzung von Schranken und Vorhersage von Relationen. Aufbauend darauf veröffentlichen wir IneqMath, einen von Experten kuratierten Datensatz von Olympiad-niveau Ungleichungen, der einen Testdatensatz und ein Trainingskorpus mit schrittweisen Lösungen und Theorem-Annotationen enthält. Wir entwickeln auch ein neuartiges LLM-as-Judge-Bewertungsframework, das einen Endantwort-Richter mit vier schrittweisen Richtern kombiniert, die darauf ausgelegt sind, häufige Denkfehler zu erkennen. Eine systematische Bewertung von 29 führenden LLMs auf IneqMath offenbart eine überraschende Realität: Selbst Spitzenmodelle wie o1 erreichen unter schrittweiser Prüfung eine Gesamtgenauigkeit von weniger als 10%; dies ist ein Rückgang von bis zu 65,5% im Vergleich zu ihrer Genauigkeit, wenn nur die Endantwortäquivalenz berücksichtigt wird. Diese Diskrepanz zeigt fragile deduktive Ketten und eine kritische Lücke bei aktuellen LLMs zwischen dem bloßen Finden einer Antwort und dem Konstruieren eines rigorosen Beweises. Die Skalierung der Modellgröße und die Erhöhung der Rechenzeit während des Tests bringen nur begrenzte Verbesserungen in der Gesamtbeweiskorrektheit. Stattdessen heben unsere Ergebnisse vielversprechende Forschungsrichtungen hervor, wie theoremgeleitetes Denken und Selbstverfeinerung. Code und Daten sind verfügbar unter https://ineqmath.github.io/.

English

Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategic theorem application. This makes it a distinct, demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing datasets that are often scarce, synthetic, or rigidly formal. We address this by proposing an informal yet verifiable task formulation, recasting inequality proving into two automatically checkable subtasks: bound estimation and relation prediction. Building on this, we release IneqMath, an expert-curated dataset of Olympiad-level inequalities, including a test set and training corpus enriched with step-wise solutions and theorem annotations. We also develop a novel LLM-as-judge evaluation framework, combining a final-answer judge with four step-wise judges designed to detect common reasoning flaws. A systematic evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even top models like o1 achieve less than 10% overall accuracy under step-wise scrutiny; this is a drop of up to 65.5% from their accuracy considering only final answer equivalence. This discrepancy exposes fragile deductive chains and a critical gap for current LLMs between merely finding an answer and constructing a rigorous proof. Scaling model size and increasing test-time computation yield limited gains in overall proof correctness. Instead, our findings highlight promising research directions such as theorem-guided reasoning and self-refinement. Code and data are available at https://ineqmath.github.io/.

Lösen von Ungleichheitsbeweisen mit großen Sprachmodellen

Solving Inequality Proofs with Large Language Models

Zusammenfassung

Support