論文の概要: Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
- arxiv url: http://arxiv.org/abs/2604.16538v1
- Date: Thu, 16 Apr 2026 21:15:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-21 21:52:52.060376
- Title: Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
- Title（参考訳）: リーン形式化のためのツール強化エージェントを理解する:要因分析
- Authors: Ke Zhang, Patricio Gallardo, Maziar Raissi, Sudhir Murthy,
- Abstract要約: 本研究では,自然言語をリーン4コードに変換するツール拡張エージェントの有効性について検討する。
まず、エージェントをワンショットベースラインに対してベンチマークし、コンパイルの成功とセマンティックな等価性の両方に大きな効果を示す。
次に、因子分解を用いて、各ツールタイプの影響を定量化し、各ツールタイプの限界貢献を全体的なパフォーマンスに分離します。
- 参考スコア（独自算出の注目度）: 6.42941089713711
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automatic translation of natural language mathematics into faithful Lean 4 code is hindered by the fundamental dissonance between informal set-theoretic intuition and strict formal type theory. This gap often causes LLMs to hallucinate non-existent library definitions, resulting in code that fails to compile or lacks semantic fidelity. In this work, we investigate the effectiveness of tool-augmented agents for this task through a systematic factorial analysis of three distinct tool categories: Fine-tuned Model Querying (accessing expert drafts), Knowledge Search (retrieving symbol definitions), and Compiler Feedback (verifying code via a Lean REPL). We first benchmark the agent against one-shot baselines, demonstrating large gains in both compilation success and semantic equivalence. We then use the factorial decomposition to quantify the impact of each category, isolating the marginal contribution of each tool type to overall performance.
- Abstract（参考訳）: 自然言語数学の忠実なリーン4コードへの自動翻訳は、非公式な集合論的な直観と厳密な形式的型理論の基本的な不協和によって妨げられる。
このギャップはしばしば、LLMが既存のライブラリ定義を幻覚させ、コンパイルに失敗したり、セマンティックな忠実さを欠いたコードをもたらす。
本研究では,細調整モデルクエリ(エキスパートドラフトへのアクセス),知識検索(シンボル定義の検索),コンパイラフィードバック(リーンREPLによるコードの検証)という,3つの異なるツールカテゴリの系統的要因分析を通じて,このタスクに対するツール強化エージェントの有効性について検討する。
まず、エージェントをワンショットベースラインに対してベンチマークし、コンパイルの成功とセマンティックな等価性の両方に大きな効果を示す。
次に、因子分解を用いて各カテゴリの影響を定量化し、各ツールタイプの限界寄与を全体的なパフォーマンスに分離する。
関連論文リスト
- METER: Evaluating Multi-Level Contextual Causal Reasoning in Large Language Models [61.33372454250959]
コンテキスト因果推論は、大規模言語モデルにとって重要なが難しい能力である。
既存のベンチマークでは、コンテキスト整合性を保証するか、完全な因果階層をカバーすることができない。
私たちはMETERの先駆者であり、因果はしごの3つのレベルすべてにわたってLSMを体系的にベンチマークしました。
論文 参考訳（メタデータ） (2026-04-13T14:07:11Z) - From Restructuring to Stabilization: A Large-Scale Experiment on Iterative Code Readability Refactoring with Large Language Models [5.31828955342405]
大規模言語モデル(LLM)は、自動化されたコードタスクにますます使われています。
この記事では、コード可読性のためのLLMの能力を体系的に研究する。
論文 参考訳（メタデータ） (2026-02-25T12:05:25Z) - LLMs Explain't: A Post-Mortem on Semantic Interpretability in Transformer Models [3.7965260744113163]
大きな言語モデル(LLM)は、その汎用性と強力なパフォーマンスのために、広範にコンピューティングで人気が高まっている。
本稿では,LLMにおいて言語的抽象化がどのように現れるのかを考察し,異なるモジュール間で言語的抽象化を検出することを目的とする。
注意に基づく説明は、後層表現がトークンに対応しているというコア仮定をテストすると、崩壊します。
埋め込みに適用される特性推論法も、その高い予測スコアが、方法論的アーティファクトとデータセット構造によって駆動されたため失敗した。
論文 参考訳（メタデータ） (2026-01-30T12:46:37Z) - How Different Tokenization Algorithms Impact LLMs and Transformer Models for Binary Code Analysis [0.0]
その重要性にもかかわらず、アセンブリコードのコンテキストにおけるトークン化は未探索領域のままである。
我々は、アセンブリコードのユニークな特徴に合わせて、プリプロセスのカスタマイズオプションとプリトークン化ルールについて検討する。
我々は,トークン化効率,語彙圧縮,組立符号の表現忠実度に基づくトークン化器の比較を行った。
論文 参考訳（メタデータ） (2025-11-05T19:45:26Z) - CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
我々は,系統的かつ包括的な推論プロセスを実行するためのモデルを導くことで,モデルがよりきめ細やかで正確な絞り込み決定を実行できることを提案する。
我々は,(i)クレームの分解,(ii)サブクレームの属性と包含分類,および(iii)集約分類から成る3段階の推論プロセスを定義し,そのような導出推論が実際に幻覚検出の改善をもたらすことを示す。
論文 参考訳（メタデータ） (2025-06-05T17:02:52Z) - A Tool for In-depth Analysis of Code Execution Reasoning of Large Language Models [1.644043499620662]
本稿では,コード実行推論フレームワークの結果を分析する一連のツールであるExeRScopeを紹介する。
分析は、より多くのベンチマークを設計することなく、同様の特性を持つコードに一般化することができる。
論文 参考訳（メタデータ） (2025-01-30T16:56:08Z) - Evaluating Human Alignment and Model Faithfulness of LLM Rationale [66.75309523854476]
大規模言語モデル(LLM)が,その世代を理論的にどのように説明するかを考察する。
提案手法は帰属に基づく説明よりも「偽り」が少ないことを示す。
論文 参考訳（メタデータ） (2024-06-28T20:06:30Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳（メタデータ） (2023-10-23T17:58:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。