論文の概要: Evaluating Program Semantics Reasoning with Type Inference in System F
- arxiv url: http://arxiv.org/abs/2509.23686v2
- Date: Mon, 20 Oct 2025 22:38:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-25 03:08:10.536244
- Title: Evaluating Program Semantics Reasoning with Type Inference in System F
- Title(参考訳): システムFにおける型推論を用いたプログラムセマンティック推論の評価
- Authors: Yifeng He, Luning Yang, Christopher Castro Gaw Gonzalo, Hao Chen,
- Abstract要約: 大規模言語モデル(LLM)は、ソフトウェアエンジニアリングエコシステムにますます統合されています。
本稿では,システムFの型推論に基づいてLLM推論を評価するベンチマークであるTF-Benchを紹介する。
TF-Bench_pureは、純粋に意味論的に駆動されるTF-Benchの変種である。
- 参考スコア(独自算出の注目度): 5.6064011695311455
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) are increasingly integrated into the software engineering ecosystem. Their test-time compute (TTC) reasoning capabilities show significant potential for understanding program logic and semantics beyond mere token recognition. However, current benchmarks for code reasoning lack a formal, program-centric deductive framework to ensure sound evaluation, and are incapable of assessing whether models genuinely reason about program semantics or merely exploit superficial associations between natural language and code tokens. To bridge this gap, we introduce TF-Bench, a benchmark designed to evaluate LLM reasoning based on type inference in System F, a task we refer to as program semantics reasoning. By employing verified transformations to remove semantically irrelevant natural language, we construct TF-Bench_pure, a purely semantics-driven variant of TF-Bench. Our analysis reveals substantial limitations in state-of-the-art LLMs, with the best-performing LLM (Claude-3.7-sonnet) achieving only 55.85% accuracy on TF-Bench_pure. Additionally, we propose two novel metrics to assess robustness and the effectiveness of test-time reasoning, underscoring critical limitations in current LLM capabilities and highlighting essential directions for future research.
- Abstract(参考訳): 大規模言語モデル(LLM)は、ソフトウェアエンジニアリングエコシステムにますます統合されています。
テスト時間計算(TTC)推論能力は、単なるトークン認識以上のプログラムロジックやセマンティクスを理解する大きな可能性を示している。
しかし、現在のコード推論のベンチマークでは、健全な評価を保証するための形式的なプログラム中心の推論フレームワークが欠如しており、モデルがプログラムの意味論について真に理由付けしているか、それとも単に自然言語とコードトークン間の表面的関連性を利用するのかを評価することができない。
このギャップを埋めるために,システムFの型推論に基づくLSM推論を評価するためのベンチマークTF-Benchを導入する。
検証された変換を用いて意味的に無関係な自然言語を除去し、純粋に意味論的に駆動されるTF-Benchの変種であるTF-Bench_pureを構築する。
TF-Bench_pureで55.85%の精度しか達成できないLLM(Claude-3.7-sonnet)を最適性能で実現した。
さらに、テスト時間推論の有効性とロバスト性を評価するための2つの新しい指標を提案し、現在のLLM能力の限界を強調し、今後の研究に欠かせない方向性を強調した。
関連論文リスト
- Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳(メタデータ) (2025-10-29T15:30:31Z) - DivLogicEval: A Framework for Benchmarking Logical Reasoning Evaluation in Large Language Models [58.439517684779936]
本稿では,多種多様な文からなる自然文からなる古典論理ベンチマークDivLogicEvalを提案する。
また,より信頼性の高い評価を実現するために,大規模言語モデルに固有のバイアスやランダム性の影響を緩和する新たな評価指標を導入する。
論文 参考訳(メタデータ) (2025-09-19T04:40:46Z) - Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。
最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。
本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
論文 参考訳(メタデータ) (2025-09-02T14:16:02Z) - Computational Reasoning of Large Language Models [51.629694188014064]
textbfTuring Machine Benchは,Large Language Models(LLM)による推論プロセスの実行能力を評価するベンチマークである。
TMBenchには、自己完結型および知識に依存しない推論、最小主義的な多段階構造、制御可能な難易度、チューリングマシンに基づく理論的基礎の4つの重要な特徴が組み込まれている。
論文 参考訳(メタデータ) (2025-04-29T13:52:47Z) - Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference [0.9319432628663639]
大規模言語モデル(LLM)は、プログラミングタスクの自動化にますます使われています。
本稿では,プログラム意味論におけるLLMの推論能力を評価するためのベンチマークであるFormalBenchを紹介する。
このベンチマークを用いて、一貫した仕様と完全な仕様を合成するLLMの能力を評価した。
論文 参考訳(メタデータ) (2025-02-22T13:27:31Z) - Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment [21.12989936864145]
CoT(Chain-of-Thought)のプロンプトによって,大規模言語モデル(LLM)の推論能力の向上が期待できる。
本稿では、生成したプログラムと対応するNL記述との間に論理単位を整列させることにより、より信頼性の高い推論経路を構築するReasoning-as-Logic-Units (RaLU)を提案する。
論文 参考訳(メタデータ) (2025-02-05T08:23:18Z) - Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
大規模言語モデル(LLM)は自然言語処理に革命をもたらしたが、一貫性のない推論に苦戦している。
本研究では,LLM出力の信頼性と透明性を高めるフレームワークであるProof of Thoughtを紹介する。
主な貢献は、論理的整合性を高めるためのソート管理を備えた堅牢な型システム、事実的知識と推論的知識を明確に区別するための規則の明示である。
論文 参考訳(メタデータ) (2024-09-25T18:35:45Z) - LLMs for Relational Reasoning: How Far are We? [8.840750655261251]
大規模言語モデル(LLM)は、下流タスクで最先端のパフォーマンスを達成することで、多くの領域に革命をもたらした。
近年の取り組みにより,LSMは逐次決定問題の解決に乏しいことが示されている。
論文 参考訳(メタデータ) (2024-01-17T08:22:52Z) - CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。
このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。
LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
論文 参考訳(メタデータ) (2023-11-29T08:29:54Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。