論文の概要: O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis

• arxiv url: http://arxiv.org/abs/2510.12350v2
• Date: Thu, 16 Oct 2025 13:07:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-17 14:17:28.093966
• Title: O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis
• Title（参考訳）: O-Forge: 漸近解析のためのLLM + Computer Algebraフレームワーク
• Authors: Ayush Khaitan, Vijay Ganesh,
• Abstract要約: 大規模言語モデルは、最近、IMOとPutnamの問題を解決する高度な能力を実証した。 主な困難は検証である: 提案は妥当に見えるが、厳密なチェックなしには信頼できない。 コンピュータ代数システムとフロンティア LLM を結合する LLM+CAS というフレームワークを提案する。
• 参考スコア（独自算出の注目度）: 5.6900369690933195
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models have recently demonstrated advanced capabilities in solving IMO and Putnam problems; yet their role in research mathematics has remained fairly limited. The key difficulty is verification: suggested proofs may look plausible, but cannot be trusted without rigorous checking. We present a framework, called LLM+CAS, and an associated tool, O-Forge, that couples frontier LLMs with a computer algebra systems (CAS) in an In-Context Symbolic Feedback loop to produce proofs that are both creative and symbolically verified. Our focus is on asymptotic inequalities, a topic that often involves difficult proofs and appropriate decomposition of the domain into the "right" subdomains. Many mathematicians, including Terry Tao, have suggested that using AI tools to find the right decompositions can be very useful for research-level asymptotic analysis. In this paper, we show that our framework LLM+CAS turns out to be remarkably effective at proposing such decompositions via a combination of a frontier LLM and a CAS. More precisely, we use an LLM to suggest domain decomposition, and a CAS (such as Mathematica) that provides a verification of each piece axiomatically. Using this loop, we answer a question posed by Terence Tao: whether LLMs coupled with a verifier can be used to help prove intricate asymptotic inequalities. More broadly, we show how AI can move beyond contest math towards research-level tools for professional mathematicians.
• Abstract（参考訳）: 大規模言語モデルは、最近、IMOとパットナムの問題を解決する高度な能力を示したが、研究数学におけるその役割はかなり限られている。 重要な難しさは検証である: 提案された証明は妥当に見えるが、厳密なチェックなしでは信用できない。 本稿では,LLM+CASと呼ばれるフレームワークと,それに関連するツールであるO-Forgeについて述べる。 我々の焦点は漸近的不等式(asymsymotic inequalities)であり、しばしば難しい証明とドメインを「右」サブドメインに適切に分解するトピックである。 テリー・タオを含む多くの数学者は、適切な分解を見つけるためにAIツールを使用することは、研究レベルの漸近解析に非常に有用であると示唆している。 本稿では, LLM+CAS をフロンティア LLM と CAS を組み合わせることで, これらの分解を効果的に提案できることを示す。 より正確には、LLMを用いてドメイン分解を提案し、各ピースを公理的に検証するCAS(Mathematicaなど)を提供する。 このループを用いて、テレンス・タオ(英語版)が提起した質問に答える: 検証子と結合された LLM が、複雑な漸近的不等式を証明するのに役立つかどうか。 より広い範囲で、AIは、プロの数学者のための研究レベルのツールへと、競争数学を超えて進むことができることを示す。

関連論文リスト

• 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 [75.95179490687018]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• Large Language Models for Mathematical Analysis [3.7325315394927023]
  この研究は、数学的推論における重要なギャップに対処し、信頼できるAIの進歩に寄与する。 DEMI-MathAnalysisデータセットを開発した。 また,LLMの問題解決能力を高めるためのガイドフレームワークも設計した。
  論文  参考訳（メタデータ） (2024-12-28T20:37:55Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAPは、それらの算術的証明構造に関する仕様に従って、問題文と連鎖推論トレースを生成する。 MathGAP を用いて, LLM はより深く, より広くなるにつれて, 性能が著しく低下することがわかった。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• 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)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)

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

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