論文の概要: IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
- arxiv url: http://arxiv.org/abs/2512.00997v1
- Date: Sun, 30 Nov 2025 17:40:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-02 19:46:34.534075
- Title: IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
- Title（参考訳）: IndiMathBench:人間のタッチによる数学的推論問題の自動生成
- Authors: Param Biyani, Shashank Kirtania, Yasharth Bajpai, Sumit Gulwani, Ashish Tiwari,
- Abstract要約: IndiMathBenchは、数学的定理の証明を評価するために設計された人間検証ベンチマークである。
IndiMathBenchは312の形式的Lean 4定理とそれに対応する非公式な問題文を組み合わせて構成されている。
- 参考スコア（独自算出の注目度）: 8.80477323574638
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce IndiMathBench, a human-verified benchmark designed to evaluate mathematical theorem proving, curated using an AI-powered human-assisted pipeline for formalizing natural language problems in Lean. IndiMathBench is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads. Through category-based retrieval, iterative compiler feedback, and multi-model ensembles, our pipeline generates candidate formalizations that experts efficiently validate via an interactive dashboard with automated quality summaries. Evaluation across multiple frontier models demonstrates that autoformalization remains challenging, with substantial gaps between syntactic validity and semantic correctness, while theorem proving success rates remain low even with iterative refinement, demonstrating that \benchmark~presents a challenging testbed for mathematical reasoning. IndiMathBench is available at https://github.com/prmbiy/IndiMathBench.
- Abstract（参考訳）: IndiMathBenchは、AIによる人力支援パイプラインを用いて、AIによる自然言語問題の定式化を図った数学的定理証明を評価するために設計された人間検証ベンチマークである。
IndiMathBenchは312の形式的Lean 4定理とそれに対応する非公式な問題文を組み合わせて構成されている。
カテゴリベースの検索,反復的コンパイラフィードバック,マルチモデルアンサンブルを通じて,我々のパイプラインは,自動品質要約を備えた対話型ダッシュボードを通じて,専門家が効果的に検証する候補形式を生成する。
複数のフロンティアモデルによる評価は、自己形式化は、構文的妥当性と意味論的正当性の間にかなりのギャップがあるままであり、一方で、反復的洗練においても成功率を証明する定理は低いままであり、'benchmark</a>は数学的推論の難しいテストベッドであることを示している。
IndiMathBenchはhttps://github.com/prmbiy/IndiMathBench.comで入手できる。
関連論文リスト
- Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。
本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。
我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
論文 参考訳（メタデータ） (2025-08-21T14:15:40Z) - Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems [9.041749463376599]
本稿では,自然言語の数学的コーパスから高品質な証明中心ベンチマークを合成するフレームワークProof2Hybridを提案する。
我々のフレームワークとベンチマークは、AIシステムの数学的インテリジェンスに関する、より深い研究の波の道を開く。
論文 参考訳（メタデータ） (2025-08-04T08:59:36Z) - 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) - PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。
提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。
提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
論文 参考訳（メタデータ） (2025-03-04T06:32:30Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - 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) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳（メタデータ） (2023-02-24T03:28:46Z) - NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。
NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。
数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
論文 参考訳（メタデータ） (2021-03-24T03:14:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。