論文の概要: FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4

• arxiv url: http://arxiv.org/abs/2503.03238v1
• Date: Wed, 05 Mar 2025 07:34:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-06 15:53:40.924246
• Title: FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4
• Title（参考訳）: FANS - Lean4を用いた自然言語数学推論のための公式回答選択
• Authors: Jiarui Yao, Ruida Wang, Tong Zhang,
• Abstract要約: FANS: Lean4を用いた自然言語数学推論のための形式的アンサー選択法を提案する。 LLMの算数推論能力を高めるためにLean4を使用した最初のフレームワークである。 LLMのNL数学能力を強化し、その正解をコンピュータで検証できるソリューションを提供する。
• 参考スコア（独自算出の注目度）: 9.732905760042193
• License:
• Abstract: Large Language Models (LLMs) have displayed astonishing abilities in various tasks, especially in text generation, classification, question answering, etc. However, the reasoning ability of LLMs still faces many debates. The inherent ambiguity of Natural Language (NL) limits LLMs' ability to perform verifiable reasoning, making its answers lack coherence and trustworthy support. To tackle the above problems, we propose a novel framework named FANS: Formal ANswer Selection for Natural Language Math Reasoning Using Lean4. To the best of our knowledge, it is the first framework that utilizes Lean4 to enhance LLMs' NL math reasoning ability. In particular, given an NL math question and LLM-generated answers, FANS first translates it into Lean4 theorem statements. Then it tries to prove it using a Lean4 prover and verify it by Lean4. Finally, it uses the FL result to assist in answer selection. It enhances LLMs' NL math ability in providing a computer-verifiable solution for its correct answer and proposes an alternative method for answer selection beyond the reward model. Extensive experiments indicate the effectiveness of our framework. It can improve the accuracy rate of reward model enhanced LLMs in the MATH-500 dataset by at most 1.91% and AMC-23 by at most 8.33% on strong reward-model baselines. In some particular fields like number theory that Lean4 experts in, we can even select all correct solutions. The qualitative analysis also shows our framework can make NL results formally backed by Lean4 proofs. As a pioneering work in the corresponding field, we will open-source all our models and datasets to further boost the development of the field.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、テキスト生成、分類、質問応答など、様々なタスクにおいて驚くべき能力を示している。 しかし、LLMの推論能力はいまだに多くの議論に直面している。 自然言語(NL)固有の曖昧さは、LLMが検証可能な推論を行う能力を制限し、その答えには一貫性と信頼できるサポートが欠如している。 上記の問題に対処するため、我々はFANSという新しいフレームワークを提案している。 私たちの知る限りでは、LLMのNL算術推論能力を高めるためにLean4を利用する最初のフレームワークです。 特に、NL の数学問題と LLM の解が与えられた場合、FANS はまずそれを Lean4 の定理文に変換する。 そして、Lean4の証明器を使ってそれを証明し、Lean4で検証します。 最後に、FL結果を用いて回答の選択を支援する。 LLMの正解に対するコンピュータ検証可能なソリューションを提供するためのNL算術能力を強化し、報酬モデルを超えた解選択のための代替手法を提案する。 大規模な実験は、我々のフレームワークの有効性を示している。 MATH-500データセットの報酬モデル強化LSMの精度を少なくとも1.91%、AMC-23は8.33%向上できる。 Lean4の専門家が参加する数論のような特定の分野では、正しいソリューションを全て選択できるのです。 質的な分析は、私たちのフレームワークがLean4の証明によって公式にNLの結果を裏付けることができることを示している。 対応する分野における先駆的な取り組みとして、私たちは、フィールドの開発をさらに促進するために、すべてのモデルとデータセットをオープンソース化します。

関連論文リスト

• CLR-Bench: Evaluating Large Language Models in College-level Reasoning [17.081788240112417]
  大規模言語モデル(LLM)は、様々な言語理解タスクで顕著な性能を示した。 複雑な大学レベルの推論において,LLMを包括的に評価するためにCLR-Benchを提案する。
  論文  参考訳（メタデータ） (2024-10-23T04:55:08Z)
• GIVE: Structured Reasoning of Large Language Models with Knowledge Graph Inspired Veracity Extrapolation [108.2008975785364]
  Graph Inspired Veracity Extrapolation (GIVE)は、パラメトリックメモリと非パラメトリックメモリを融合して、最小の外部入力で正確な推論を改善する新しい推論手法である。 GIVE は LLM エージェントをガイドして,最も関連する専門家データ (observe) を選択し,クエリ固有の発散思考 (reflect) に従事し,その情報を合成して最終的な出力 (speak) を生成する。
  論文  参考訳（メタデータ） (2024-10-11T03:05:06Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Perception of Knowledge Boundary for Large Language Models through Semi-open-ended Question Answering [67.94354589215637]
  大きな言語モデル(LLM)は知識探索に広く用いられているが、幻覚に悩まされている。 本稿では,LLMの知識境界(KB)を半オープンな質問(SoeQ)で知覚する。 GPT-4 は SoeQ では性能が悪く,KB に気づいていないことが多い。 我々の補助モデルであるLLaMA-2-13Bは、より曖昧な答えを見つけるのに有効である。
  論文  参考訳（メタデータ） (2024-05-23T10:00:14Z)
• Can LLMs Master Math? Investigating Large Language Models on Math Stack Exchange [25.419977967846144]
  大規模言語モデル(LLM)は、様々な自然言語タスクにおいて例外的な機能を示した。 本稿では、複雑な数学的問題解決をナビゲートする上でのLLMの限界について考察する。
  論文  参考訳（メタデータ） (2024-03-30T12:48:31Z)
• Supervised Knowledge Makes Large Language Models Better In-context Learners [94.89301696512776]
  大規模言語モデル(LLM)は、素早い工学を通して、文脈内学習能力の出現を示す。 自然言語理解と質問応答におけるLLMの一般化性と事実性の向上という課題は、まだ未解決のままである。 本研究では, LLM の信頼性を高める枠組みを提案する。1) 分布外データの一般化,2) 差別モデルによる LLM のメリットの解明,3) 生成タスクにおける幻覚の最小化。
  論文  参考訳（メタデータ） (2023-12-26T07:24:46Z)
• The ART of LLM Refinement: Ask, Refine, and Trust [85.75059530612882]
  ART: Ask, Refine, and Trust と呼ばれる改良目標を用いた推論を提案する。 LLMがいつその出力を洗練すべきかを決めるために必要な質問を尋ねる。 自己補充ベースラインよりも+5ポイントの性能向上を達成する。
  論文  参考訳（メタデータ） (2023-11-14T07:26:32Z)
• Knowing What LLMs DO NOT Know: A Simple Yet Effective Self-Detection Method [36.24876571343749]
  大規模言語モデル(LLM)は自然言語処理(NLP)タスクにおいて大きな可能性を示している。 近年の文献では、LLMは断続的に非実効応答を生成する。 本研究では,LLM が知らない質問が非現実的な結果を生成する傾向にあることを検知する新たな自己検出手法を提案する。
  論文  参考訳（メタデータ） (2023-10-27T06:22:14Z)
• LaGR-SEQ: Language-Guided Reinforcement Learning with Sample-Efficient Querying [71.86163159193327]
  大規模言語モデル(LLM)は、最近、テキストを介してコンテキスト対応の応答を提供するという、印象的な能力を実証した。 この能力は、パターン補完に関連するシーケンシャルな意思決定タスクにおいて、妥当なソリューションを予測するために使われる可能性がある。 第一強化学習(RL)エージェントによって部分的に完了したタスクに対する解を提案するために,LLMのこの予測能力を利用するLaGRを紹介した。
  論文  参考訳（メタデータ） (2023-08-21T02:07:35Z)
• Statistical Knowledge Assessment for Large Language Models [79.07989821512128]
  ファクトイドの問題に関する様々なプロンプトを考慮すれば、大きな言語モデル(LLM)は事実的に正しい答えを確実に生成できるだろうか? LLMの事実知識を評価する統計的手法であるKaRRを提案する。 この結果から,同じバックボーン構造を持つLLMの知識はスケーリング法則に則っており,命令追従データに基づくチューニングは,実際に正しいテキストを確実に生成するモデルの能力を損なう場合があることがわかった。
  論文  参考訳（メタデータ） (2023-05-17T18:54:37Z)

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

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