論文の概要: Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery

• arxiv url: http://arxiv.org/abs/2606.08728v1
• Date: Sun, 07 Jun 2026 16:50:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-09 14:42:06.418778
• Title: Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
• Title（参考訳）: 数学的推論のための人工知能:言語モデル、ニューロシンボリックシステム、検証された発見の総合的な調査
• Authors: Syed Rifat Raiyan, Mohsinul Kabir, Hasan Mahmud, Md Kamrul Hasan,
• Abstract要約: この調査は、この分野の進化の統一的な説明を提供する。 i)テキストや図面に対する非公式な推論、MWPの解法、マルチモーダル幾何、RLMの解法、(ii)自動形式化、戦術予測、コンパイラ誘導修理、証明探索を含む証明アシスタントの形式的推論、(iii)システム構築の提案、境界の改善、オープンな問題に対する攻撃を支援する数学的発見、(iv)CoTプロンプト、ツールの使用、プロセス報酬モデル、VLVRなど、推論およびトレーニング時のテクニック。
• 参考スコア（独自算出の注目度）: 3.9943798586374784
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Mathematical reasoning has long served as a stringent test of machine intelligence; over the past decade, it has moved from a niche problem within NLP to one of the most consequential AI frontiers. This survey provides a unified account of the field's evolution, from early rule-based math word problem (MWP) solvers and template-driven geometry systems, through neural expression generation and LLM prompting, to contemporary reasoning models, multi-agent systems, neuro-symbolic theorem provers, and verified discovery workflows. We organize the landscape along four axes: (i) informal reasoning over text and diagrams, spanning MWP solving, multimodal geometry, and VLMs; (ii) formal reasoning in proof assistants, including autoformalization, tactic prediction, compiler-guided repair, and proof search; (iii) mathematical discovery, where systems propose constructions, improve bounds, or assist attacks on open problems; and (iv) the inference and training-time techniques, including CoT prompting, tool use, process reward models, and RLVR, that increasingly connect generation with verification. We catalog major benchmarks across grade-school arithmetic, competition mathematics, geometry, formal proving, multimodal and multilingual reasoning, and expert evaluation, and we examine benchmark saturation, contamination, reporting mismatches, and the distinction between pass@1, majority voting, and verifier-assisted pass@$k$. We critically assess failure modes: brittleness under perturbation, reward hacking, multimodal grounding failures, fragile formalization, and the energy cost of reasoning-scale inference. Drawing on recent perspectives from working mathematicians, we identify future directions centered on verified-discovery workflows, reasoning efficiency, and infrastructure to make AI-assisted formalization broadly usable. Companion materials: https://github.com/Starscream-11813/awesome-AI4Math.
• Abstract（参考訳）: 過去10年間、NLP内のニッチな問題から、最も重要なAIフロンティアの1つに移行してきた。 このサーベイは、初期のルールベースの数学語問題(MWP)の解法とテンプレート駆動幾何システムから、ニューラル表現の生成とLLMプロンプト、現代の推論モデル、マルチエージェントシステム、ニューロシンボリック定理プロバー、検証された発見ワークフローまで、分野の進化の統一的な説明を提供する。 私たちは4つの軸に沿って風景を整理します。 一 テキスト及び図面の非公式な推論、MWP解決、マルチモーダル幾何学及びVLM 二 自動書式化、戦術予測、コンパイラ誘導修理及び証明探索を含む証明助手の形式的推論 三 数学的な発見で、システムが建設を提案し、限界を改善し、又はオープンな問題に対する攻撃を支援すること。 (4)CoTプロンプト,ツール使用,プロセス報酬モデル,RLVRなど,世代と検証を結び付ける推論とトレーニング時間のテクニック。 我々は,小学生算術,競争数学,幾何,形式証明,マルチモーダルおよび多言語推論,専門家評価の各ベンチマークをカタログ化し,ベンチマーク飽和,汚染,報告ミスマッチ,パス@1,多数決,検証支援パス@$k$の区別について検討する。 我々は、摂動下での脆さ、報酬ハッキング、マルチモーダルグラウンド障害、脆弱な形式化、推論スケール推論のエネルギーコストなど、障害モードを批判的に評価する。 作業数学者の最近の見解に基づいて、検証済みのワークフロー、推論効率、そしてAI支援の形式化を広く利用できるようにするインフラに焦点を絞った将来の方向性を特定する。 関連資料:https://github.com/Starscream-11813/awesome-AI4Math

関連論文リスト

• Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics [9.38309744591661]
  フォーマル・コンジェクチャ(Formal Conjectures)は、Lean 4.0で形式化された2615の数学的問題文の進化ベンチマークである。 このデータセットは、数学的な証明発見のためのゼロ汚染ベンチマークを提供する1029のオープンリサーチ予想を特徴としている。 我々は,これらの形式化の正しさを保証するためのアプローチを,アクティブなコミュニティからのコントリビューションを生かしたオープンソースプロジェクトとして紹介する。
  論文  参考訳（メタデータ） (2026-05-13T08:33:15Z)
• Automated Conjecture Resolution with Formal Verification [21.763678203045973]
  本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。 我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。 このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
  論文  参考訳（メタデータ） (2026-04-04T16:35:16Z)
• Deconstructing Multimodal Mathematical Reasoning: Towards a Unified Perception-Alignment-Reasoning Paradigm [82.57296908195654]
  MMR(Multimodal Mathematical Reasoning)は、テキストと視覚の両方のモダリティを含む数学的問題を解く能力に注目が集まっている。 現在のモデルは、実世界の視覚数学のタスクにおいて大きな課題に直面している。
  論文  参考訳（メタデータ） (2026-03-09T12:11:00Z)
• Systematic Diagnosis of Brittle Reasoning in Large Language Models [1.14219428942199]
  人工知能における中心的な問題は、機械学習モデルが数学を理解する範囲である。 本稿では,特定の故障点を診断するために,標準ベンチマークを超えて数学的推論を計測する新しい枠組みを提案する。
  論文  参考訳（メタデータ） (2025-10-05T21:40:09Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)
• Large Language Models as Analogical Reasoners [155.9617224350088]
  CoT(Chain-of- Thought)は、言語モデルのプロンプトとして、推論タスク全体で素晴らしいパフォーマンスを示す。 そこで本稿では,大規模言語モデルの推論プロセスを自動的にガイドする,新たなプロンプト手法であるアナログプロンプトを導入する。
  論文  参考訳（メタデータ） (2023-10-03T00:57:26Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• Machine Number Sense: A Dataset of Visual Arithmetic Problems for Abstract and Relational Reasoning [95.18337034090648]
  文法モデルを用いて自動生成される視覚的算術問題からなるデータセット、MNS(Machine Number Sense)を提案する。 これらの視覚的算術問題は幾何学的フィギュアの形をしている。 我々は、この視覚的推論タスクのベースラインとして、4つの主要なニューラルネットワークモデルを用いて、MNSデータセットをベンチマークする。
  論文  参考訳（メタデータ） (2020-04-25T17:14:58Z)

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

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