論文の概要: Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification

• arxiv url: http://arxiv.org/abs/2509.23061v1
• Date: Sat, 27 Sep 2025 02:33:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 22:32:19.016766
• Title: Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
• Title（参考訳）: 局所的な成功は構成しない: 構成形式検証のための大規模言語モデルのベンチマーク
• Authors: Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan,
• Abstract要約: DafnyCOMPは、Dafnyにおける構成仕様生成において、大きな言語モデル(LLM)を評価するためのベンチマークである。 現状のLLMファミリーを複数評価し, 単機能検証では良好に機能するが, 構成タスクでは顕著に低下することがわかった。
• 参考スコア（独自算出の注目度）: 21.987735608080374
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-function tasks, DafnyCOMP targets programs composed of multiple interacting functions with data dependencies, requiring reasoning across component boundaries. The benchmark consists of 300 automatically synthesized multi-function programs. We evaluate several state-of-the-art LLM families and find that, while they perform well on single-function verification, their performance drops sharply on compositional tasks. Analysis reveals systematic failures in cross-functional reasoning, including fragile specifications, misalignment between implementations and proofs, and unstable reasoning. DafnyCOMP thus provides a diagnostic tool for measuring progress toward reliable, verifiable, and compositional code generation with LLMs.
• Abstract（参考訳）: Dafnyの仕様生成において,大規模言語モデル(LLM)を評価するためのベンチマークであるDafnyCOMPを紹介する。 単一機能タスクにフォーカスする以前のベンチマークとは異なり、DafnyCOMPは複数のインタラクション関数とデータ依存関係で構成されるプログラムをターゲットにしており、コンポーネント境界を越えて推論する必要がある。 ベンチマークは300個の自動合成多機能プログラムで構成されている。 現状のLLMファミリーを複数評価し, 単機能検証では良好に機能するが, 構成タスクでは顕著に低下することがわかった。 分析は、脆弱な仕様、実装と証明のミスアライメント、不安定な推論など、クロスファンクショナルな推論における体系的な失敗を明らかにしている。 従って、DafnyCOMPは、LLMによる信頼性、検証、および構成コード生成に向けた進捗を測定するための診断ツールを提供する。

関連論文リスト

• Visual Document Understanding and Question Answering: A Multi-Agent Collaboration Framework with Test-Time Scaling [83.78874399606379]
  テスト時間スケーリングを備えたマルチエージェント協調フレームワークであるMACTを提案する。 4つの異なる小規模エージェントから構成され、明確に定義された役割と効果的なコラボレーションがある。 一般および数学的タスクの能力を犠牲にすることなく、より小さなパラメータスケールで優れた性能を示す。
  論文  参考訳（メタデータ） (2025-08-05T12:52:09Z)
• CORE: Benchmarking LLMs Code Reasoning Capabilities through Static Analysis Tasks [12.465309397733249]
  大規模言語モデル(LLM)は様々なソフトウェア工学領域で広く採用されている。 これらのアプリケーションは、表面レベルのコードパターン以上の理解を必要とします。 既存のベンチマークは、コードが正しく修正されるか、生成されたかといったエンドツーエンドの結果を主に評価する。
  論文  参考訳（メタデータ） (2025-07-03T01:35:58Z)
• A Large Language Model-Empowered Agent for Reliable and Robust Structural Analysis [14.754785659805869]
  大規模言語モデル(LLM)は、様々なオープンドメインタスクにまたがる顕著な能力を示してきたが、土木工学のような専門分野への応用は、いまだに未解明のままである。 本稿では, ビーム構造解析におけるLCMの信頼性とロバスト性を評価することによって, このギャップを埋める。 実験の結果, エージェントはベンチマークデータセット上で99.0%を超える精度を達成し, 多様な条件で信頼性と堅牢性を示すことがわかった。
  論文  参考訳（メタデータ） (2025-06-27T04:16:53Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• IDA-Bench: Evaluating LLMs on Interactive Guided Data Analysis [60.32962597618861]
  IDA-Benchは、多ラウンドの対話シナリオで大規模言語モデルを評価する新しいベンチマークである。 エージェント性能は、最終的な数値出力と人間由来のベースラインを比較して判断する。 最先端のコーディングエージェント(Claude-3.7-thinkingなど)でさえ50%のタスクを成功させ、シングルターンテストでは明らかでない制限を強調している。
  論文  参考訳（メタデータ） (2025-05-23T09:37:52Z)
• LLMDFA: Analyzing Dataflow in Code with Large Language Models [8.92611389987991]
  本稿では,コンパイル不要でカスタマイズ可能なデータフロー解析フレームワークLLMDFAを提案する。 問題をいくつかのサブタスクに分解し、一連の新しい戦略を導入する。 LLMDFAは平均87.10%の精度と80.77%のリコールを達成し、F1スコアを最大0.35に向上させた。
  論文  参考訳（メタデータ） (2024-02-16T15:21:35Z)
• FactCHD: Benchmarking Fact-Conflicting Hallucination Detection [64.4610684475899]
  FactCHD は LLM からファクトコンフリクトの幻覚を検出するために設計されたベンチマークである。 FactCHDは、バニラ、マルチホップ、比較、セット操作など、さまざまな事実パターンにまたがる多様なデータセットを備えている。 Llama2 に基づくツール強化 ChatGPT と LoRA-tuning による反射的考察を合成する Truth-Triangulator を提案する。
  論文  参考訳（メタデータ） (2023-10-18T16:27:49Z)
• Discover, Explanation, Improvement: An Automatic Slice Detection Framework for Natural Language Processing [72.14557106085284]
  スライス検出モデル(SDM)は、データポイントの低パフォーマンスなグループを自動的に識別する。 本稿では,NLPタスクの分類のための "Discover, Explain, improve (DEIM)" というベンチマークを提案する。 評価の結果,Edisaは情報的セマンティックな特徴を持つ誤り発生データポイントを正確に選択できることがわかった。
  論文  参考訳（メタデータ） (2022-11-08T19:00:00Z)

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

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