대형 언어 모델을 활용한 부등식 증명 해결

초록

불평등 증명은 다양한 과학 및 수학 분야에서 중요한 역할을 하며, 엄밀한 경계를 발견하고 전략적으로 정리를 적용하는 등 고급 추론 능력을 시험합니다. 이는 대규모 언어 모델(LLM)에게 일반적인 수학 문제 해결을 넘어선 통찰력을 제공하는 독특하고 까다로운 분야로 자리 잡고 있습니다. 그러나 이 분야의 발전은 기존 데이터셋이 부족하거나 합성적이며, 지나치게 형식적인 경우가 많아 저해받고 있습니다. 우리는 이를 해결하기 위해 비공식적이지만 검증 가능한 과제 구성을 제안하며, 불평등 증명을 자동으로 검사 가능한 두 가지 하위 과제인 경계 추정과 관계 예측으로 재구성합니다. 이를 바탕으로, 우리는 올림피아드 수준의 불평등 문제를 전문가가 선별한 IneqMath 데이터셋을 공개합니다. 이 데이터셋은 테스트 세트와 단계별 해결 방법 및 정리 주석이 포함된 훈련 코퍼스를 포함하고 있습니다. 또한, 우리는 최종 답안 판단자와 일반적인 추론 오류를 탐지하도록 설계된 네 명의 단계별 판단자를 결합한 새로운 LLM-as-judge 평가 프레임워크를 개발했습니다. IneqMath에서 29개의 주요 LLM을 체계적으로 평가한 결과, 놀라운 현실이 드러났습니다: 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/.

대형 언어 모델을 활용한 부등식 증명 해결

Solving Inequality Proofs with Large Language Models

초록

Support