Решение доказательств неравенств с использованием больших языковых моделей

Solving Inequality Proofs with Large Language Models

June 9, 2025

Авторы: Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, Pan Lu

cs.AI

Аннотация

Доказательство неравенств, имеющее ключевое значение в различных научных и математических областях, проверяет продвинутые навыки рассуждения, такие как нахождение точных границ и стратегическое применение теорем. Это делает его уникальной и сложной задачей для больших языковых моделей (LLM), предлагая инсайты, выходящие за рамки общего решения математических задач. Прогресс в этой области затруднен из-за существующих наборов данных, которые часто являются скудными, синтетическими или чрезмерно формализованными. Мы решаем эту проблему, предлагая неформальную, но проверяемую формулировку задачи, преобразуя доказательство неравенств в две автоматически проверяемые подзадачи: оценку границ и предсказание отношений. На основе этого мы выпускаем IneqMath, экспертно составленный набор данных олимпиадного уровня, включающий тестовый набор и обучающий корпус, обогащенный пошаговыми решениями и аннотациями теорем. Мы также разрабатываем новую систему оценки LLM-as-judge, сочетающую судью, проверяющего окончательный ответ, с четырьмя пошаговыми судьями, предназначенными для выявления типичных ошибок в рассуждениях. Систематическая оценка 29 ведущих LLM на IneqMath выявляет удивительную реальность: даже лучшие модели, такие как o1, демонстрируют менее 10% общей точности при пошаговой проверке; это снижение до 65,5% по сравнению с их точностью, учитывающей только эквивалентность окончательного ответа. Это расхождение выявляет хрупкие дедуктивные цепочки и критический разрыв для современных LLM между простым нахождением ответа и построением строгого доказательства. Увеличение размера модели и вычислительных ресурсов во время тестирования дают ограниченный прирост в общей корректности доказательств. Вместо этого наши результаты указывают на перспективные направления исследований, такие как рассуждения, основанные на теоремах, и самоусовершенствование. Код и данные доступны по адресу 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/.