論文の概要: An Empirical Study of LLM-Generated Specifications for VeriFast
- arxiv url: http://arxiv.org/abs/2606.26490v1
- Date: Thu, 25 Jun 2026 00:50:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-26 18:46:32.123631
- Title: An Empirical Study of LLM-Generated Specifications for VeriFast
- Title（参考訳）: VeriFastのLCM生成仕様に関する実証的研究
- Abstract要約: 静的検証ツールは、産業規模のソフトウェアを保証できますが、仕様を書くにはかなりの人的労力が必要です。
最近の研究は、検証対象の仕様を含むコード、テスト、証明を生成するために、大きな言語モデル(LLM)を適用している。
本稿では,SL検証器 VeriFast で 303 C 関数を検証するための仕様を生成するために LLM がいかにうまく機能するかを徹底的に評価する。
- 参考スコア（独自算出の注目度）: 7.58397933941565
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Static verification tools can assure industrial scale software, but require significant human labor to write specifications. This is particularly true of static verifiers based on separation logic (SL verifiers), which excel at verifying heapmanipulating programs, but require many complex auxiliary specifications to reason about heap structure. Recent work applies large language models (LLMs) to generate code, tests, and proofs, including specifications for verifiers, but mostly targeting non-SL verifiers. To address this gap, this paper thoroughly evaluates how well LLMs perform when prompted to generate specifications for verifying 303 C functions with the SL verifier VeriFast. We explored eight prompting approaches, ten LLMs, and three input types in two stages. Quantitative and qualitative analyses are used to assess the LLM-generated code and specifications for functional behavior, verifiability and errors. The results show that LLMs preserve functional behavior in source code and specifications (both over 91%), but achieve modest verification success (31.4%). Using Gemini 2.5 Pro and providing formal contracts lead to higher success rates in our setting. Moreover, most errors (94%) come from LLMs' mistakes in the domainspecific knowledge of SL verifiers such as VeriFast. These findings provide guidance for optimizing LLM-generated specifications for SL verifiers.
- Abstract（参考訳）: 静的検証ツールは、産業規模のソフトウェアを保証できますが、仕様を書くにはかなりの人的労力が必要です。
これは、分離論理(SL検証)に基づく静的検証には特に当てはまり、ヒープ操作プログラムの検証に優れるが、ヒープ構造を推論するためには、多くの複雑な補助的な仕様を必要とする。
最近の研究は、コード、テスト、証明を生成するために大規模な言語モデル(LLM)を適用している。
このギャップに対処するため、SL検証器VeriFastで303のC関数を検証するための仕様を生成するために、LLMがいかにうまく機能するかを徹底的に評価する。
提案手法は,8つのプロンプトアプローチ,10個のLDM,3つの入力タイプを2段階に分けて検討した。
定量的かつ質的な分析は、LCMの生成したコードと機能的振る舞い、検証可能性、エラーの仕様を評価するために用いられる。
結果は、LLMはソースコードと仕様(どちらも91%以上)の機能的振る舞いを保っているが、適度な検証成功(31.4%)を達成していることを示している。
Gemini 2.5 Proを使用し、正式な契約を提供することで、私たちの環境での成功率を高めます。
さらに、ほとんどのエラー(94%)は、VeriFastのようなSL検証器のドメイン固有知識におけるLLMの誤りに由来する。
これらの結果は,SL検証器のLCM生成仕様を最適化するためのガイダンスを提供する。
関連論文リスト
- ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。
ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。
1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
論文 参考訳（メタデータ） (2026-07-01T09:58:59Z) - Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。
より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。
そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
論文 参考訳（メタデータ） (2026-02-28T08:35:25Z) - Uncovering Systematic Failures of LLMs in Verifying Code Against Natural Language Specifications [0.6813925418351435]
大規模言語モデル(LLM)はソフトウェア開発において不可欠なツールとなり、要求工学、コード生成、レビュータスクに広く利用されている。
本稿では,LLMが自然言語の要求に適合するかどうかを評価する上で,体系的に失敗していることを明らかにする。
以上の結果から,LCMは要件を満たすことのできないコード実装や潜在的な欠陥を含むコード実装を誤って分類することが多いことが判明した。
論文 参考訳（メタデータ） (2025-08-17T13:07:26Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - AGENTIF: Benchmarking Instruction Following of Large Language Models in Agentic Scenarios [51.46347732659174]
LLM(Large Language Models)は、現実世界のエージェントアプリケーションにおいて高度な機能を示す。
AgentIFは、エージェントシナリオでLLM命令に従う能力を体系的に評価する最初のベンチマークである。
論文 参考訳（メタデータ） (2025-05-22T17:31:10Z) - Extracting Formal Specifications from Documents Using LLMs for Automated Testing [11.129512305353055]
正式な仕様を定義する主なアプローチは、ソフトウェア文書のマニュアル分析である。
システム更新は、対応する正式な仕様を維持するための人件費をさらに高める。
大規模言語モデルの最近の進歩は、自然言語理解において有望な能力を示している。
論文 参考訳（メタデータ） (2025-04-02T01:58:11Z) - Next Steps in LLM-Supported Java Verification [0.8057006406834466]
大きな言語モデル(LLM)はコード生成に適したツールであるだけでなく、アノテーションベースのコード仕様を生成することもできる。
本稿では、この厳密なツールセットを用いて、信頼できないLCMから正しい仕様アノテーションを確実に取り出す方法について、初期の結果を提供する。
論文 参考訳（メタデータ） (2025-02-03T17:55:50Z) - ToolScan: A Benchmark for Characterizing Errors in Tool-Use LLMs [77.79172008184415]
TOOLSCANは、ツール使用タスクのLLM出力におけるエラーパターンを特定するための新しいベンチマークである。
もっとも顕著なLCMでも,これらの誤りパターンが出力に現れることを示す。
研究者たちは、TOOLSCANのこれらの洞察を使って、エラー軽減戦略をガイドすることができる。
論文 参考訳（メタデータ） (2024-11-20T18:56:22Z) - SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
大規模言語モデル(LLM)は、適切な自然言語プロンプトを提供する際に、多様なタスクを解決するという約束を持っている。
学生LLMからタスク固有の入出力ペアを合成する多段階メカニズムであるSELF-GUIDEを提案する。
ベンチマークの指標から,分類タスクに約15%,生成タスクに18%の絶対的な改善を報告した。
論文 参考訳（メタデータ） (2024-07-16T04:41:58Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳（メタデータ） (2023-11-15T14:41:57Z) - Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。
LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。
LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
論文 参考訳（メタデータ） (2023-10-15T12:40:30Z) - Configuration Validation with Large Language Models [22.018488540410548]
大きな言語モデル(LLM)は、MLベースの構成検証の長期的制限に対処する上で、有望であることを示している。
汎用的なLCMベースの構成検証フレームワークCiriを開発した。
Ciriは有効なプロンプトエンジニアリングを採用し、有効な設定データと設定ミスデータの両方に基づいて数ショットの学習を行う。
論文 参考訳（メタデータ） (2023-10-15T00:50:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。