論文の概要: CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

• arxiv url: http://arxiv.org/abs/2605.17255v1
• Date: Sun, 17 May 2026 04:53:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-19 17:57:47.811373
• Title: CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
• Title（参考訳）: CAM-Bench: リーンにおける計算数学と応用数学のベンチマーク
• Authors: Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen,
• Abstract要約: CAM-Benchは、計算および応用数学における1000のリーン証明目標のLean 4定理証明ベンチマークである。 これらの問題は教科書の演習に適応しており、しばしばローカルに導入された定義、表記法、アルゴリズム、基礎的な結果に依存している。 リーンコンパイルとセマンティックレビューを通じて、結果のフォーマルな問題を検証し、フォーマルな正当性とセマンティックなアライメントの両方を元のエクササイズで確認します。
• 参考スコア（独自算出の注目度）: 10.684401671916158
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal theorem-proving benchmarks enable mechanically verifiable evaluation of mathematical reasoning in large language models. However, existing benchmarks mainly focus on Olympiad-style problems and algebraic domains, leaving computational and applied mathematics underrepresented. We introduce CAM-Bench, a Lean 4 theorem-proving benchmark of 1,000 Lean proof targets in computational and applied mathematics, with coverage spanning optimization, numerical linear algebra, and numerical analysis. These problems are adapted from textbook exercises and often depend on locally introduced definitions, notation, algorithms, and elementary results. To construct CAM-Bench, we develop a dependency-recovery pipeline that reconstructs the local textbook context needed to state each problem faithfully. It then normalizes each problem into a standalone informal theorem and translates it into a Lean target. We validate the resulting formal problems through Lean compilation and semantic review, checking both formal correctness and semantic alignment with the original exercises. For each problem, we release the raw exercise, recovered context, normalized informal theorem, and final Lean target. CAM-Bench complements existing formal mathematics benchmarks by targeting applied mathematics problems that rely on textbook concepts and elementary theorems, many of which are not directly available as standard Mathlib4 lemmas. We evaluate widely used large language models and formalization agents on CAM-Bench, and analyze common failure modes in tracking local assumptions, applying elementary results, decomposing proofs, and maintaining long-horizon control in Lean.
• Abstract（参考訳）: 形式的定理証明ベンチマークは、大きな言語モデルにおける数学的推論の機械的検証を可能にする。 しかし、既存のベンチマークは主にオリンピアード形式の問題と代数的領域に焦点を当てており、計算や応用数学は不足している。 CAM-Benchは、計算および応用数学における1000のリーン証明対象のLean 4定理を実証するベンチマークであり、カバレッジは最適化、数値線形代数、数値解析にまたがる。 これらの問題は教科書の演習に適応しており、しばしばローカルに導入された定義、表記法、アルゴリズム、基礎的な結果に依存している。 CAM-Benchを構築するために,各問題を忠実に記述するために必要な局所的な教科書コンテキストを再構築する依存性回復パイプラインを開発した。 そして、各問題をスタンドアローンの非公式な定理に正規化し、それをリーンの目標に翻訳します。 リーンコンパイルとセマンティックレビューを通じて、結果のフォーマルな問題を検証し、フォーマルな正当性とセマンティックなアライメントの両方を元のエクササイズで確認します。 それぞれの問題に対して、生のエクササイズ、回復されたコンテキスト、正規化された非公式な定理、最終的なリーン目標をリリースします。 CAM-Benchは、教科書の概念や基本定理に依存する応用数学問題をターゲットにして、既存の形式数学のベンチマークを補完する。 我々は,CAM-Bench上で広く使用されている大規模言語モデルと形式化エージェントを評価し,局所的な仮定の追跡,基本結果の適用,証明の分解,リーンにおける長期制御の維持などにおいて,一般的な障害モードを分析した。

関連論文リスト

• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。 本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。 公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
  論文  参考訳（メタデータ） (2026-03-13T07:39:47Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。 さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
  論文  参考訳（メタデータ） (2026-01-30T15:24:42Z)
• IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch [8.80477323574638]
  IndiMathBenchは、数学的定理の証明を評価するために設計された人間検証ベンチマークである。 IndiMathBenchは312の形式的Lean 4定理とそれに対応する非公式な問題文を組み合わせて構成されている。
  論文  参考訳（メタデータ） (2025-11-30T17:40: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)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)

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

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