論文の概要: Thinking Machines: Mathematical Reasoning in the Age of LLMs

• arxiv url: http://arxiv.org/abs/2508.00459v1
• Date: Fri, 01 Aug 2025 09:31:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-04 18:08:53.815587
• Title: Thinking Machines: Mathematical Reasoning in the Age of LLMs
• Title（参考訳）: 思考機械:LLM時代の数学的推論
• Authors: Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen,
• Abstract要約: 大規模言語モデル(LLM)は構造化推論や記号的タスクにおいて顕著な能力を示している。 この記事では、最近のモデルとベンチマークに焦点を当て、機械学習と数学的認知の交差における3つの中心的な課題について考察する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) have shown remarkable abilities in structured reasoning and symbolic tasks, with coding emerging as a particular area of strength. This success has sparked growing interest in applying LLMs to mathematics, both in informal problem-solving and formal theorem proving. However, progress in formal mathematics has proven to be significantly more difficult, despite surface-level similarities between programming and proof construction. This discrepancy raises important questions about how LLMs ``reason'', how they are supervised, and whether they internally track a notion of computational or deductive state. In this article, we address the state-of-the-art of the discipline, focusing on recent models and benchmarks, and explore three central issues at the intersection of machine learning and mathematical cognition: (i) the trade-offs between formal and informal mathematics as training domains; (ii) the deeper reasons why proof generation remains more brittle than code synthesis; (iii) and the question of whether LLMs represent, or merely mimic, a notion of evolving logical state. Our goal is not to draw hard boundaries, but to identify where the current limits lie, and how they might be extended.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、構造的推論や記号的タスクにおいて顕著な能力を示し、コーディングが特定の強みの領域として現れる。 この成功は、非公式な問題解決と公式な定理証明の両方において、LSMを数学に適用することへの関心が高まった。 しかし、形式数学の進歩は、プログラミングと証明構成の間に表面的な類似性があるにもかかわらず、著しく困難であることが証明されている。 この不一致は、LLMが ‘`reason'' をどのように管理するか、どのように教師されているか、そして、それらが内部的に計算的あるいは誘引的状態の概念を追跡しているのか、という重要な疑問を提起する。 本稿では、最近のモデルとベンチマークに注目し、機械学習と数学的認知の交差における3つの中心的な課題を探求する。 一 訓練領域としての形式数学と形式数学のトレードオフ (二 コード合成より証明生成が脆弱であることの深い理由 3) LLM は進化的論理状態の概念を表わすか、あるいは単に模倣するかという問題である。 私たちのゴールは、ハードバウンダリを引き出すのではなく、現在の限界がどこにあるのか、どのように拡張されるのかを特定することです。

関連論文リスト

• Comprehension Without Competence: Architectural Limits of LLMs in Symbolic Computation and Reasoning [7.996731257791417]
  大型言語モデル (LLM) は、記号的推論、算術的精度、論理的整合性を必要とするタスクにおいて、表面流速が著しく低下するが、体系的に失敗する。 本稿では,このような障害の構造的診断を行い,テキスト理解とテキストコンピテンスの間に持続的なギャップがあることを明らかにする。 我々はこの現象を,命令経路と行動経路が幾何学的に,機能的に二分される計算テキストスプリット・ブレイン症候群と呼ぶ。
  論文  参考訳（メタデータ） (2025-07-14T04:01:45Z)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  計算思考モデル(CTM)は、計算思考パラダイムを大規模言語モデル(LLM)に組み込んだ新しいフレームワークである。 ライブコード実行は推論プロセスにシームレスに統合され、CTMが計算によって考えることができる。 CTMは、精度、解釈可能性、一般化可能性の観点から、従来の推論モデルとツール拡張ベースラインを上回っている。
  論文  参考訳（メタデータ） (2025-06-03T09:11:15Z)
• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning [27.562284768743694]
  大規模言語モデル(LLM)は、証明システム内で証明ステップを生成することによって、数学的定理を正式に証明することができる。 本稿では,LLMが学習した数学的直観と,記号的手法によって符号化された領域固有の洞察を相乗化する,ニューロシンボリック・戦術生成器を提案する。 複数の数学コンペティションから161の挑戦的不等式を評価する。
  論文  参考訳（メタデータ） (2025-02-19T15:54:21Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
  大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。 1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。 このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
  論文  参考訳（メタデータ） (2024-02-29T15:26:14Z)
• Evaluating LLMs' Mathematical and Coding Competency through Ontology-guided Interventions [47.83142414018448]
  算術的推論とコード生成という,2つの一般的な推論タスクに注目します。 i) 数学やコーディング問題に対する摂動の一般的なオントロジー, (ii) 摂動を応用するための半自動手法, (iii) 2つのデータセットを紹介する。 混乱した質問に対して、すべてのモデルで大幅なパフォーマンス低下を示します。
  論文  参考訳（メタデータ） (2024-01-17T18:13:07Z)
• 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 are In-Context Semantic Reasoners rather than Symbolic Reasoners [75.85554779782048]
  大規模言語モデル(LLM)は、近年、自然言語と機械学習コミュニティを興奮させています。 多くの成功を収めたアプリケーションにもかかわらず、そのようなコンテキスト内機能の基盤となるメカニズムはまだ不明である。 本研究では,学習した言語トークンのテクストセマンティクスが推論過程において最も重い処理を行うと仮定する。
  論文  参考訳（メタデータ） (2023-05-24T07:33:34Z)

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

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