論文の概要: MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification

• arxiv url: http://arxiv.org/abs/2512.18256v1
• Date: Sat, 20 Dec 2025 07:39:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-23 18:54:32.258527
• Title: MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
• Title（参考訳）: MSC-180: 数学的対象分類に基づく自動形式理論のベンチマーク
• Authors: Sirui Li, Wangyue Lu, Xiaorui Shi, Ke Weng, Haozhe Sun, Minghe Yu, Tiancheng Zhang, Ge Yu, Hengyu Liu, Lun Du,
• Abstract要約: 現在の大言語モデル(LLM)に基づく定理証明は、制限された領域カバレッジや数学的推論の弱い一般化といった制限に悩まされている。 我々は,MSC 2020の数学的対象分類に基づく評価ベンチマークであるMSC-180を提案する。 180の形式的検証問題、60の数学分野から3つの先進的な問題が含まれており、学部から大学院まで多岐にわたる。
• 参考スコア（独自算出の注目度）: 21.9173105378467
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated Theorem Proving (ATP) represents a core research direction in artificial intelligence for achieving formal reasoning and verification, playing a significant role in advancing machine intelligence. However, current large language model (LLM)-based theorem provers suffer from limitations such as restricted domain coverage and weak generalization in mathematical reasoning. To address these issues, we propose MSC-180, a benchmark for evaluation based on the MSC2020 mathematical subject classification. It comprises 180 formal verification problems, 3 advanced problems from each of 60 mathematical branches, spanning from undergraduate to graduate levels. Each problem has undergone multiple rounds of verification and refinement by domain experts to ensure formal accuracy. Evaluations of state-of-the-art LLM-based theorem provers under the pass@32 setting reveal that the best model achieves only an 18.89% overall pass rate, with prominent issues including significant domain bias (maximum domain coverage 41.7%) and a difficulty gap (significantly lower pass rates on graduate-level problems). To further quantify performance variability across mathematical domains, we introduce the coefficient of variation (CV) as an evaluation metric. The observed CV values are 4-6 times higher than the statistical high-variability threshold, indicating that the models still rely on pattern matching from training corpora rather than possessing transferable reasoning mechanisms and systematic generalization capabilities. MSC-180, together with its multi-dimensional evaluation framework, provides a discriminative and systematic benchmark for driving the development of next-generation AI systems with genuine mathematical reasoning abilities.
• Abstract（参考訳）: ATP(Automated Theorem Proving)は、正式な推論と検証を達成するための人工知能のコア研究の方向性であり、人工知能の進歩に重要な役割を果たしている。 しかし、現在の大言語モデル(LLM)に基づく定理証明は、制限されたドメインカバレッジや数学的推論の弱い一般化といった制限に悩まされている。 これらの問題に対処するため,MSC2020の数学的対象分類に基づく評価ベンチマークであるMSC-180を提案する。 180の形式的検証問題と、60の数学分野から3つの先進的な問題が含まれており、学部から大学院にまたがっている。 それぞれの問題は、正式な正確性を保証するために、ドメインの専門家による検証と改善を繰り返してきた。 パス@32設定による最先端のLCMベースの定理証明器の評価によると、最良のモデルは18.89%のパス率しか達成していないが、顕著なドメインバイアス(最大ドメインカバレッジ41.7%)と難易度ギャップ(特に大学院レベルの問題に対するパスレートが低い)を含む顕著な問題がある。 数学領域における性能変動の定量化のために,評価指標として変動係数(CV)を導入する。 観測されたCV値は統計的高変量閾値の4～6倍であり, モデルが伝達可能な推論機構や系統的一般化能力を持つのではなく, トレーニングコーパスからのパターンマッチングに依存していることが示唆された。 MSC-180は多次元評価フレームワークとともに、真の数学的推論能力を持つ次世代AIシステムの開発を推進するための差別的で体系的なベンチマークを提供する。

関連論文リスト

• The Catastrophic Paradox of Human Cognitive Frameworks in Large Language Model Evaluation: A Comprehensive Empirical Analysis of the CHC-LLM Incompatibility [0.0]
  平均的な人間のIQスコアを達成するモデルは、結晶化された知識タスクにおいてゼロに近づいた二分精度を同時に示す。 この切断は、結晶化されたインテリジェンス領域において最も強く現れる。 人工知能の非人間性を認識するネイティブマシン認識アセスメントを開発するための枠組みを提案する。
  論文  参考訳（メタデータ） (2025-11-23T05:49:57Z)
• Max It or Miss It: Benchmarking LLM On Solving Extremal Problems [0.0]
  数学的極端問題を解くためのベンチマークデータセットExtremBenchを紹介する。 我々は、Qwen3、GPT-OSS、DeepSeekなど、最先端のオープンソースモデルファミリーで評価を行う。 その結果、LLMの極端解法推論能力は、現在の数学ベンチマークと必ずしも一致しないことがわかった。
  論文  参考訳（メタデータ） (2025-10-14T21:23:37Z)
• Beyond Overall Accuracy: A Psychometric Deep Dive into the Topic-Specific Medical Capabilities of 80 Large Language Models [6.362188639024662]
  項目応答理論(IRT)に基づく厳密な評価フレームワークであるtextscMedIRT を紹介する。 80の多種多様な言語モデル (LLMs) から, バランスのとれた1,100のUSMLE準拠のベンチマークで, 新たな回答を期待して収集した。 LLMの潜在モデル能力は質問の難易度や識別と共同で推定し、精度のみよりも安定でニュアンスの高い性能ランキングを得る。
  論文  参考訳（メタデータ） (2025-09-29T02:06:13Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。 OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
  論文  参考訳（メタデータ） (2025-03-27T11:20:17Z)
• ErrorRadar: Benchmarking Complex Mathematical Reasoning of Multimodal Large Language Models Via Error Detection [60.297079601066784]
  エラー検出におけるMLLMの能力を評価するために設計された最初のベンチマークであるErrorRadarを紹介する。 ErrorRadarはエラーステップ識別とエラー分類という2つのサブタスクを評価している。 2500の高品質なマルチモーダルK-12数学問題で構成され、実世界の学生相互作用から収集される。 GPT-4oの優れた性能は、まだ人間の評価に約10%遅れているため、大きな課題が残っている。
  論文  参考訳（メタデータ） (2024-10-06T14:59:09Z)
• Evaluating Mathematical Reasoning Beyond Accuracy [50.09931172314218]
  推論ステップの品質を評価するための新しい方法論であるReasonEvalを紹介します。 ReasonEvalはメタ評価データセットのベースライン手法よりも一貫して優れていることを示す。 我々は、ReasonEvalがデータ選択において重要な役割を果たすことを観察する。
  論文  参考訳（メタデータ） (2024-04-08T17:18:04Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。