大規模言語モデルを用いた不等式証明の解法

不等式証明は、多様な科学分野や数学分野において重要な役割を果たし、厳密な境界の発見や戦略的な定理の適用などの高度な推論スキルを試すものです。これは大規模言語モデル（LLMs）にとって、一般的な数学問題解決を超えた洞察を提供する独自かつ困難なフロンティアとなっています。この領域での進展は、既存のデータセットがしばしば不足していたり、合成されたり、堅苦しい形式に制限されているため阻害されています。これを解決するために、我々は非形式的でありながら検証可能なタスク設定を提案し、不等式証明を2つの自動的にチェック可能なサブタスクに再構成しました：境界推定と関係予測。此基础上，我们发布了IneqMath，这是一个由专家策划的包含奥林匹克级别不等式的データセットで、ステップバイステップの解法と定理注釈を含むテストセットと学習コーパスが含まれています。さらに、最終解答評価者と4つのステップバイステップ評価者からなる新しいLLM-as-judge評価フレームワークを開発しました。これらの評価者は一般的な推論の誤りを検出することを目指しています。29の主要なLLMについてIneqMathで系統的に評価した結果、驚くべき現実が明らかになりました：トップクラスのモデルでもo1のように、ステップバイステップの精査下では全体的な精度が10%未満となり、最終解答のみを考える場合からの精度低下は最大65.5%に達します。この乖離は脆弱な演繹チェーンと、単に答えを見つけ出すことと厳密な証明を構築することとの間における現在のLLMにとって重要なギャップを露呈しています。モデルサイズの拡大やテスト時の計算量の増加は全体的な証明正確性に限られた改善しかもたらさないことがわかりました。代わりに、我々の研究結果は定理ガイド推論や自己改良などの有望な研究方向性を示唆しています。コードとデータは https://ineqmath.github.io/ で利用可能です。（注：文中“此基础上”部分的日语翻译进行了调整以适应日语的表达习惯，同时在“o1”处保留了原文标记，因为这可能是特定模型的名称或标识符。）