論文の概要: Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions

• arxiv url: http://arxiv.org/abs/2502.12065v2
• Date: Wed, 19 Mar 2025 18:53:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-21 19:00:29.364401
• Title: Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions
• Title（参考訳）: LLMを用いた複雑な数学的ステートメントの形式化:数学的定義に関する研究
• Authors: Lan Zhang, Marco Valentino, Andre Freitas,
• Abstract要約: 我々は、ウィキペディア(Def_Wiki)とarXiv論文(Def_ArXiv)から定義を収集する、自動形式化のための2つの新しいリソースを紹介する。 我々は、Isabelle/HOLに定義を形式化する能力を解析し、LLMの範囲を評価した。 以上の結果から, miniF2Fのような既存のベンチマークと比較して, 定義がより困難であることが判明した。
• 参考スコア（独自算出の注目度）: 8.135142928659546
• License:
• Abstract: Thanks to their linguistic capabilities, LLMs offer an opportunity to bridge the gap between informal mathematics and formal languages through autoformalization. However, it is still unclear how well LLMs generalize to sophisticated and naturally occurring mathematical statements. To address this gap, we investigate the task of autoformalizing real-world mathematical definitions -- a critical component of mathematical discourse. Specifically, we introduce two novel resources for autoformalisation, collecting definitions from Wikipedia (Def_Wiki) and arXiv papers (Def_ArXiv). We then systematically evaluate a range of LLMs, analyzing their ability to formalize definitions into Isabelle/HOL. Furthermore, we investigate strategies to enhance LLMs' performance including refinement through external feedback from Proof Assistants, and formal definition grounding, where we guide LLMs through relevant contextual elements from formal mathematical libraries. Our findings reveal that definitions present a greater challenge compared to existing benchmarks, such as miniF2F. In particular, we found that LLMs still struggle with self-correction, and aligning with relevant mathematical libraries. At the same time, structured refinement methods and definition grounding strategies yield notable improvements of up to 16% on self-correction capabilities and 43% on the reduction of undefined errors, highlighting promising directions for enhancing LLM-based autoformalization in real-world scenarios.
• Abstract（参考訳）: 言語能力のおかげで、LLMは非公式数学と形式言語の間のギャップを自己形式化によって埋める機会を提供する。 しかし、LLMがいかに高度で自然発生の数学的ステートメントに一般化するかは、いまだに不明である。 このギャップに対処するために,実世界の数学的定義を自己形式化するタスクについて検討する。 具体的には、Wikipedia(Def_Wiki)とarXiv(Def_ArXiv)から定義を収集する。 次に,LLMを体系的に評価し,その定義をIsabelle/HOLに形式化する能力を解析する。 さらに、プロフアシスタントからの外部フィードバックによる改善や、形式的定義に基づく基礎化など、LLMの性能向上戦略についても検討し、そこでは、形式的な数学的ライブラリから関連するコンテキスト要素を通してLLMをガイドする。 以上の結果から, miniF2Fのような既存のベンチマークと比較して, 定義がより困難であることが判明した。 特に,LLMは依然として自己補正に苦慮し,関連する数学的ライブラリと整合していることが判明した。 同時に、構造化された精細化手法と定義基盤戦略により、自己補正能力が最大16%向上し、未定義エラーが43%削減された。

関連論文リスト

• 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)
• Enriching Ontologies with Disjointness Axioms using Large Language Models [5.355177558868206]
  大型モデル(LLM)は、クラス不整合公理を識別し、主張することで一貫性を提供する。 本研究の目的は,LLMに埋め込まれた暗黙の知識を活用して,存在論的不一致を分類することである。 以上の結果から, LLMは効果的なプロンプト戦略によって導かれることにより, 不整合性関係を確実に識別できることが示唆された。
  論文  参考訳（メタデータ） (2024-10-04T09:00:06Z)
• S^3cMath: Spontaneous Step-level Self-correction Makes Large Language Models Better Mathematical Reasoners [23.713779973116733]
  自己補正は,大規模言語モデル(LLM)の潜在的な推論能力を刺激する手法である 本稿では,S$3$c-Mathを提案する。
  論文  参考訳（メタデータ） (2024-09-03T01:40:21Z)
• Potential and Limitations of LLMs in Capturing Structured Semantics: A Case Study on SRL [78.80673954827773]
  大きな言語モデル(LLM)は、言語理解を高め、解釈可能性を改善し、バイアスを減らすために構造化セマンティクスをキャプチャする上で重要な役割を果たす。 セマンティック・ロール・ラベルリング(SRL)を,構造化意味論を抽出するLLMの能力を探るための基本課題として用いることを提案する。 LLMは実際にセマンティック構造をキャプチャすることができ、スケールアップは常にポテンシャルを反映するわけではない。 エラーのかなりの重複は、LLMと訓練されていない人間の両方によって行われ、全てのエラーの約30%を占めることに私たちは驚いています。
  論文  参考訳（メタデータ） (2024-05-10T11:44:05Z)
• FAC$^2$E: Better Understanding Large Language Model Capabilities by Dissociating Language and Cognition [56.76951887823882]
  大規模言語モデル(LLM)は、主に様々なテキスト理解および生成タスクにおける全体的なパフォーマンスによって評価される。 FAC$2$E, FAC$2$Eについて述べる。
  論文  参考訳（メタデータ） (2024-02-29T21:05:37Z)
• Characterizing Truthfulness in Large Language Model Generations with Local Intrinsic Dimension [63.330262740414646]
  大規模言語モデル(LLM)から生成されたテキストの真偽を特徴付ける方法と予測法について検討する。 モデルアクティベーションの局所固有次元 (LID) を用いて, 内部アクティベーションを調査し, LLMの真偽を定量化する。
  論文  参考訳（メタデータ） (2024-02-28T04:56:21Z)
• Evaluating LLMs' Mathematical Reasoning in Financial Document Question Answering [53.56653281752486]
  本研究では,大言語モデルによる4つの財務質問応答データセットの数学的推論について検討する。 数理推論のステップの数が増えるにつれて、テーブルの複雑さや性能の変化に対する感度に焦点をあてる。 半構造化文書に適した新しいプロンプト技術を導入する。
  論文  参考訳（メタデータ） (2024-02-17T05:10:18Z)
• Beyond Words: A Mathematical Framework for Interpreting Large Language Models [8.534513717370434]
  大規模言語モデル(LLM)は、自然言語テキストやその他の複雑な情報を生成し、理解することのできる強力なAIツールである。 我々は、幻覚、アライメント、自己検証、思考の連鎖推論など、LLM研究における重要な用語と概念を明確にするフレームワークであるHexを提案する。 我々は、生成AIシステムを構築する方法についての議論を進める上で、私たちの正式な定義と結果が不可欠であると主張する。
  論文  参考訳（メタデータ） (2023-11-06T11:13:17Z)
• Improving Open Information Extraction with Large Language Models: A Study on Demonstration Uncertainty [52.72790059506241]
  オープン情報抽出(OIE)タスクは、構造化されていないテキストから構造化された事実を抽出することを目的としている。 一般的なタスク解決手段としてChatGPTのような大きな言語モデル(LLM)の可能性にもかかわらず、OIEタスクの最先端(教師付き)メソッドは遅れている。
  論文  参考訳（メタデータ） (2023-09-07T01:35:24Z)

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

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