論文の概要: Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters

• arxiv url: http://arxiv.org/abs/2503.12686v2
• Date: Tue, 30 Sep 2025 01:21:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-01 17:09:03.950024
• Title: Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
• Title（参考訳）: LLMにおける形式的推論失敗を抽象的解釈として理解する
• Authors: Jacqueline L. Mitchell, Brian Hyeongseok Kim, Chenyu Zhou, Chao Wang,
• Abstract要約: 大規模言語モデル(LLM)からそのような推論を導き出すための2つの新しいプロンプト戦略を導入する。 ソフトウェア検証に広く用いられているSV-COMPベンチマークスイートから,22のプログラムに対して,最先端のLCMを用いてこれらの戦略を評価する。
• 参考スコア（独自算出の注目度）: 5.468061853910803
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) are increasingly used for program verification, and yet little is known about \emph{how} they reason about program semantics during this process. In this work, we focus on abstract interpretation based-reasoning for invariant generation and introduce two novel prompting strategies that aim to elicit such reasoning from LLMs. We evaluate these strategies across several state-of-the-art LLMs on 22 programs from the SV-COMP benchmark suite widely used in software verification. We analyze both the soundness of the generated invariants and the key thematic patterns in the models' reasoning errors. This work aims to highlight new research opportunities at the intersection of LLMs and program verification for applying LLMs to verification tasks and advancing their reasoning capabilities in this application.
• Abstract（参考訳）: 大規模言語モデル (LLMs) は、プログラム検証にますます使われているが、このプロセス中にプログラムのセマンティクスを推論する「emph{how}」についてはほとんど知られていない。 本研究では、不変生成のための抽象的解釈に基づく推論に着目し、LLMからそのような推論を引き出すための2つの新しいプロンプト戦略を導入する。 ソフトウェア検証に広く用いられているSV-COMPベンチマークスイートから,22のプログラムに対して,最先端のLCMを用いてこれらの戦略を評価する。 生成した不変量の音質とモデルの推論誤差におけるキーテーマパターンの両方を解析する。 本研究は, LLMの共通点における新たな研究機会と, LLMを検証タスクに適用するためのプログラム検証, およびそれらの推論能力を向上することを目的とする。

関連論文リスト

• 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)
• Evaluating the Correctness of Inference Patterns Used by LLMs for Judgment [53.17596274334017]
  我々は,LLMの詳細な推論パターンの正確さを,その正しい出力の裏側で評価した。 実験により、言語生成結果が正しそうであっても、LLMが法的な判断に用いた推論パターンのかなりの部分は、誤解を招く論理や無関係な論理を表す可能性があることが示された。
  論文  参考訳（メタデータ） (2024-10-06T08:33:39Z)
• Can Large Language Models Understand Symbolic Graphics Programs? [136.5639211254501]
  シンボリックグラフィックスプログラムはコンピュータグラフィックスで人気がある。 シンボルグラフィックプログラムの意味的視覚的理解のためのベンチマークを作成する。 LLMの推理性能は概して優れていた。
  論文  参考訳（メタデータ） (2024-08-15T17:59:57Z)
• Large Language Models are Interpretable Learners [53.56735770834617]
  本稿では,Large Language Models(LLM)とシンボルプログラムの組み合わせによって,表現性と解釈可能性のギャップを埋めることができることを示す。 自然言語プロンプトを持つ事前訓練されたLLMは、生の入力を自然言語の概念に変換することができる解釈可能な膨大なモジュールセットを提供する。 LSPが学んだ知識は自然言語の記述と記号規則の組み合わせであり、人間(解釈可能)や他のLLMに容易に転送できる。
  論文  参考訳（メタデータ） (2024-06-25T02:18:15Z)
• Can LLM Graph Reasoning Generalize beyond Pattern Memorization? [46.93972334344908]
  我々は,大規模言語モデル (LLM) が,合成学習データにおける意味的,数値的,構造的,推論パターンを超えうるか否かを評価し,実世界のグラフベースタスクにおける有用性を向上させる。 トレーニング後のアライメントが現実世界のタスクに最も有望であるのに対して、LLMグラフの推論をパターンを超えて行うことは、依然としてオープンな研究課題である。
  論文  参考訳（メタデータ） (2024-06-23T02:59:15Z)
• A Survey Study on the State of the Art of Programming Exercise Generation using Large Language Models [0.0]
  本稿では,Large Language Models (LLM) のプログラミング演習生成能力について分析する。 調査研究を通じて,技術の現状を定義し,その強みと弱みを抽出し,評価行列を提案した。
  論文  参考訳（メタデータ） (2024-05-30T15:49: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)
• Rethinking Interpretability in the Era of Large Language Models [76.1947554386879]
  大規模言語モデル(LLM)は、幅広いタスクにまたがる顕著な機能を示している。 自然言語で説明できる能力により、LLMは人間に与えられるパターンのスケールと複雑さを拡大することができる。 これらの新しい機能は、幻覚的な説明や膨大な計算コストなど、新しい課題を提起する。
  論文  参考訳（メタデータ） (2024-01-30T17:38:54Z)
• LLMs for Relational Reasoning: How Far are We? [8.840750655261251]
  大規模言語モデル(LLM)は、下流タスクで最先端のパフォーマンスを達成することで、多くの領域に革命をもたらした。 近年の取り組みにより,LSMは逐次決定問題の解決に乏しいことが示されている。
  論文  参考訳（メタデータ） (2024-01-17T08:22:52Z)
• LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models [63.14196038655506]
  大規模言語モデル(LLM)の論理的推論能力を評価・拡張するための新しいアプローチであるLogicAskerを紹介する。 提案手法は, LLMが論理規則を学習する際の大きなギャップを明らかにし, 異なるモデル間で29%から90%の推論失敗を識別する。 GPT-4oのようなモデルにおける論理的推論を最大5%向上させることで、これらの知見を活用して、ターゲットとなる実演例と微調整データを構築した。
  論文  参考訳（メタデータ） (2024-01-01T13:53:53Z)
• 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)
• LMs: Understanding Code Syntax and Semantics for Code Analysis [25.508254718438636]
  我々は,大規模言語モデル(LLM)の機能と,ソフトウェア工学におけるコード解析の限界を評価する。 GPT4, GPT3.5, StarCoder, CodeLlama-13b-インストラクトという,最先端の4つの基礎モデルを採用している。
  論文  参考訳（メタデータ） (2023-05-20T08:43:49Z)

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

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