論文の概要: Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference

• arxiv url: http://arxiv.org/abs/2503.04779v3
• Date: Sat, 15 Mar 2025 10:45:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-18 12:36:13.961838
• Title: Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
• Title（参考訳）: プログラムセマンティックスについてLLMは理にかなっているか? : 形式的仕様推論に基づくLLMの包括的評価
• Authors: Thanh Le-Cong, Bach Le, Toby Murray,
• Abstract要約: 大規模言語モデル(LLM)は、プログラミングタスクの自動化にますます使われています。 本稿では,プログラム意味論におけるLLMの推論能力を評価するためのベンチマークであるFormalBenchを紹介する。 このベンチマークを用いて、一貫した仕様と完全な仕様を合成するLLMの能力を評価した。
• 参考スコア（独自算出の注目度）: 0.9319432628663639
• License:
• Abstract: Large Language Models (LLMs) are increasingly being used to automate programming tasks. Yet, LLMs' capabilities in reasoning about program semantics are still inadequately studied, leaving significant potential for further exploration. This paper introduces FormalBench, a comprehensive benchmark designed to evaluate LLMs' reasoning abilities on program semantics, particularly via the task of synthesizing formal program specifications to assist verifying program correctness. This task requires both comprehensive reasoning over all possible program executions and the generation of precise, syntactically correct expressions that adhere to formal syntax and semantics. Using this benchmark, we evaluated the ability of LLMs in synthesizing consistent and complete specifications. Our findings show that LLMs perform well with simple control flows but struggle with more complex structures, especially loops, even with advanced prompting. Additionally, LLMs exhibit limited robustness against semantic-preserving transformations. We also highlight common failure patterns and design self-repair prompts, improving success rates by 25%.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、プログラミングタスクの自動化にますます使われています。 しかし、プログラムのセマンティクスを推論するLLMの能力はまだ不十分であり、さらなる探索の可能性が残されている。 本稿では,プログラムセマンティクスにおけるLCMの推論能力を評価するための総合的なベンチマークであるFormalBenchを紹介する。 このタスクは、全ての可能なプログラムの実行に対する包括的な推論と、形式的な構文や意味論に忠実で構文的に正しい表現の生成の両方を必要とする。 このベンチマークを用いて、一貫した仕様と完全な仕様を合成するLLMの能力を評価した。 以上の結果から, LLMは単純な制御フローでは良好に機能するが, より複雑な構造, 特にループでは, 高度なプロンプトにおいても困難であることがわかった。 加えて、LLMは意味保存変換に対して限られた堅牢性を示す。 また、一般的な失敗パターンや自己修復プロンプトも強調し、成功率を25%向上させています。

関連論文リスト

• CRANE: Reasoning with constrained LLM generation [5.971462597321995]
  制約付きデコードアルゴリズムであるCRANEを提案し,制約付き生成の正しさと制約なし生成の柔軟性のバランスをとる。 CRANEは最先端の制約付き復号化戦略と標準の制約なし復号化戦略の両方を大きく上回っている。
  論文  参考訳（メタデータ） (2025-02-13T08:23:42Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications [12.683365968483807]
  プログラム仕様を用いて,大規模言語モデルにおけるコード理解を評価するためのSpecEvalを提案する。 プログラムのセマンティクスを表現し、徹底的な評価を行うために、正式な仕様を採用する。 特に、4つの仕様関連タスクは、基本的なレベルから高度なレベルまでLLMの能力を評価するように設計されている。
  論文  参考訳（メタデータ） (2024-09-19T16:08:39Z)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  大規模言語モデル(LLM)は多くの自然言語タスクにおいて印象的な能力を示している。 LLMは多段階推論を行う際にエラー、幻覚、矛盾する文を生成する傾向がある。 本稿では,LLMの復号化過程を検討計画で導くためのフレームワークであるQ*を紹介する。
  論文  参考訳（メタデータ） (2024-06-20T13:08:09Z)
• Toward Self-Improvement of LLMs via Imagination, Searching, and Criticizing [56.75702900542643]
  大規模言語モデルの自己改善のためのAlphaLLMを紹介する。 モンテカルロ木探索(MCTS)とLLMを統合し、自己改善ループを確立する。 実験の結果,AlphaLLM は付加アノテーションを使わずに LLM の性能を大幅に向上することがわかった。
  論文  参考訳（メタデータ） (2024-04-18T15:21:34Z)
• 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)
• LLMs for Relational Reasoning: How Far are We? [8.840750655261251]
  大規模言語モデル(LLM)は、下流タスクで最先端のパフォーマンスを達成することで、多くの領域に革命をもたらした。 近年の取り組みにより,LSMは逐次決定問題の解決に乏しいことが示されている。
  論文  参考訳（メタデータ） (2024-01-17T08:22:52Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
  論文  参考訳（メタデータ） (2024-01-01T16:51:20Z)
• LMs: Understanding Code Syntax and Semantics for Code Analysis [25.508254718438636]
  我々は,大規模言語モデル(LLM)の機能と,ソフトウェア工学におけるコード解析の限界を評価する。 GPT4, GPT3.5, StarCoder, CodeLlama-13b-インストラクトという,最先端の4つの基礎モデルを採用している。
  論文  参考訳（メタデータ） (2023-05-20T08:43:49Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

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

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