論文の概要: 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による信頼性、検証、および構成コード生成に向けた進捗を測定するための診断ツールを提供する。

関連論文リスト

• Deconstructing Instruction-Following: A New Benchmark for Granular Evaluation of Large Language Model Instruction Compliance Abilities [2.9203730377983654]
  既存のベンチマークでは、実際の使用を反映したり、コンプライアンスをタスクの成功から分離することができない。 アプリケーション指向の生成制約を最大20個まで含む動的に生成されたデータセットを使用するモジュール型フレームワークであるMOSAICを紹介した。 コンプライアンスはモノリシックな機能ではなく、制約タイプ、量、位置によって大きく異なります。
  論文  参考訳（メタデータ） (2026-01-26T15:02:15Z)
• Beyond Accuracy: Characterizing Code Comprehension Capabilities in (Large) Language Models [4.841487377596519]
  本稿では,Large Language Modelsのコード理解性能が従来の人間中心のソフトウェアメトリクスと一致しているかを検討する。 コード理解をバイナリインプット・アウトプット整合性タスクとして再編成する診断フレームワークを導入する。
  論文  参考訳（メタデータ） (2026-01-19T10:58:24Z)
• Matching-Based Few-Shot Semantic Segmentation Models Are Interpretable by Design [8.993770750003673]
  Few-Shot Semantic (FSS)モデルは、最小限のラベル付き例を持つ新規クラスのセグメンテーションにおいて強力な性能を達成する。 本稿では、マッチングベースのFSSモデルを解釈するための最初の専用手法を提案する。 Affinity Explainer アプローチは,画像のどのピクセルがクエリセグメンテーション予測に最も寄与しているかを示す属性マップを抽出する。
  論文  参考訳（メタデータ） (2025-11-22T19:22:10Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• 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)
• A Controllable Examination for Long-Context Language Models [62.845852724511964]
  本研究では,長文言語モデルを評価するベンチマークである$textbfLongBioBenchを紹介する。 その結果,ほとんどのモデルでは,検索結果に対する意味的理解や基礎的推論が不足していることが判明した。 我々のさらなる分析は、文脈的非コヒーレンスなど、既存の合成ベンチマークで採用されているいくつかの設計選択を示している。
  論文  参考訳（メタデータ） (2025-06-03T14:23:06Z)
• 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)
• MatPlotAgent: Method and Evaluation for LLM-Based Agentic Scientific Data Visualization [86.61052121715689]
  MatPlotAgentは、科学的データ可視化タスクを自動化するために設計された、モデルに依存しないフレームワークである。 MatPlotBenchは、100人の検証されたテストケースからなる高品質なベンチマークである。
  論文  参考訳（メタデータ） (2024-02-18T04:28:28Z)
• 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)

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

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