論文の概要: Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

• arxiv url: http://arxiv.org/abs/2502.13834v2
• Date: Tue, 25 Feb 2025 15:38:31 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-26 11:59:05.065212
• Title: Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
• Title（参考訳）: LLMの相乗化とシンボリック推論によるオリンピック不等式証明
• Authors: Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang, Xiaoxing Ma,
• Abstract要約: 大規模言語モデル(LLM)は、証明システム内で証明ステップを生成することによって、数学的定理を正式に証明することができる。 本稿では,LLMが学習した数学的直観と,記号的手法によって符号化された領域固有の洞察を相乗化する,ニューロシンボリック・戦術生成器を提案する。 複数の数学コンペティションから161の挑戦的不等式を評価する。
• 参考スコア（独自算出の注目度）: 27.562284768743694
• License:
• Abstract: Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tactics is vast and complex, while the available training data for formal proofs is limited, posing a significant challenge to LLM-based tactic generation. To address this, we introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods. The key aspect of this integration is identifying which parts of mathematical reasoning are best suited to LLMs and which to symbolic methods. While the high-level idea of neuro-symbolic integration is broadly applicable to various mathematical problems, in this paper, we focus specifically on Olympiad inequalities (Figure~1). We analyze how humans solve these problems and distill the techniques into two types of tactics: (1) scaling, handled by symbolic methods, and (2) rewriting, handled by LLMs. In addition, we combine symbolic tools with LLMs to prune and rank the proof goals for efficient proof search. We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions, achieving state-of-the-art performance and significantly outperforming existing LLM and symbolic approaches without requiring additional training data.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、証明システム内で証明ステップ(\textit{a.k.a.} 戦術)を生成することによって、数学的定理を正式に証明することができる。 しかし、可能な戦術の空間は広大で複雑であり、形式的証明のためのトレーニングデータは限られており、LSMベースの戦術生成には大きな課題がある。 そこで本研究では,LLMが学習した数学的直観と,記号的手法によって符号化されたドメイン固有の洞察を相乗化する,ニューロシンボリック・戦術生成装置を提案する。 この統合の重要な側面は、数学的推論のどの部分が LLM に最も適しており、どの部分がシンボリックな方法に適しているかを特定することである。 ニューロシンボリック積分の高レベルな考え方は、様々な数学的問題に広く適用されているが、本稿では、オリンピアードの不等式に特に焦点をあてる(図1)。 我々は,これらの問題を人間がどのように解決するかを分析し,(1)スケーリング,象徴的手法による処理,(2)書き換え,LSMによる処理の2つの方法に分類する。 さらに,記号ツールとLLMを組み合わせることで,効率的な証明探索のための証明目標を立証し,ランク付けする。 我々は,複数の数学コンペティションから不等式に挑戦する161の枠組みを評価し,最先端性能を実現し,新たなトレーニングデータを必要としない既存のLLMやシンボリックアプローチを著しく上回った。

関連論文リスト

• Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions [8.135142928659546]
  我々は、ウィキペディア(Def_Wiki)とarXiv論文(Def_ArXiv)から定義を収集する、自動形式化のための2つの新しいリソースを紹介する。 我々は、Isabelle/HOLに定義を形式化する能力を解析し、LLMの範囲を評価した。 以上の結果から, miniF2Fのような既存のベンチマークと比較して, 定義がより困難であることが判明した。
  論文  参考訳（メタデータ） (2025-02-17T17:34:48Z)
• MathFimer: Enhancing Mathematical Reasoning by Expanding Reasoning Steps through Fill-in-the-Middle Task [49.355810887265925]
  数学的推論ステップ拡張のための新しいフレームワークであるMathFimerを紹介する。 我々は、慎重にキュレートしたNuminaMath-FIMデータセットに基づいて、特殊モデルMathFimer-7Bを開発した。 次に、これらのモデルを適用して、解鎖に詳細な中間ステップを挿入することで、既存の数学的推論データセットを強化する。
  論文  参考訳（メタデータ） (2025-02-17T11:22:24Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
  証明生成のための数学的大規模言語モデルを活用することは、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)
• System-2 Mathematical Reasoning via Enriched Instruction Tuning [13.672967091915181]
  Enriched Instruction Tuning (EIT) は、人間とAIのフィードバックを相乗化することによって、既存の人間の注釈付き数学的データセットを充実させる手法である。 EITはGSM8Kで84.1%、MATHで32.5%の精度を達成し、最先端の微調整およびプロンプト法を超越している。
  論文  参考訳（メタデータ） (2024-12-22T10:49:27Z)
• Neuro-Symbolic Data Generation for Math Reasoning [47.00099724151703]
  高品質な教師付き数学的データセットを自動生成する手法を開発した。 本手法は,既存の数学問題を慎重に変更し,新たに生成した問題の多様性と妥当性を両立させる。 実験により,提案手法により生成したデータの品質を実証し,LLaMA-2 と Mistral が最先端のデータを上回ることを示した。
  論文  参考訳（メタデータ） (2024-12-06T08:49:49Z)
• Unraveling Arithmetic in Large Language Models: The Role of Algebraic Structures [3.181878085746691]
  大型言語モデル (LLM) は顕著な数学的能力を示しており、主にチェーン・オブ・シント (CoT) のプロンプトによって駆動されている。 本稿では,emphCommutativity やemphIdentity などの代数的構造を捉えることによって,LLM が算術を学習することを提案する。 この結果から,代数的構造を活用することでLLMの算術的能力が向上し,算術的性能向上への洞察が得られた。
  論文  参考訳（メタデータ） (2024-11-25T10:23:11Z)
• 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)
• Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models [56.34029644009297]
  大規模言語モデル(LLM)は、形式的知識表現(KR)システムの様々な制限を克服する能力を示した。 LLMは誘導的推論において最も優れているが、誘導的推論では最も効果が低い。 モデルの性能を評価するため,シングルタスクトレーニング,マルチタスクトレーニング,および「チェーンオブ思考」知識蒸留細調整技術について検討した。
  論文  参考訳（メタデータ） (2023-10-02T01:00:50Z)

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

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