論文の概要: Laurel: Generating Dafny Assertions Using Large Language Models

• arxiv url: http://arxiv.org/abs/2405.16792v1
• Date: Mon, 27 May 2024 03:26:01 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-28 19:16:00.305512
• Title: Laurel: Generating Dafny Assertions Using Large Language Models
• Title（参考訳）: Laurel: 大規模言語モデルを用いたダニーアサーションの生成
• Authors: Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou,
• Abstract要約: 本稿では,大規模な言語モデル(LLM)を用いて,Dafnyプログラムのヘルパーアサーションを自動的に生成するツールであるLaurillを提案する。 Laurelは数回の試行で、必要なヘルパーアサーションの50%以上を生成することができる。
• 参考スコア（独自算出の注目度）: 2.6942525604796366
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dafny is a popular verification language, which automates proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires guidance in the form of helper assertions creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that uses large language models (LLMs) to automatically generate helper assertions for Dafny programs. To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier's error message and inserting an assertion placeholder at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new lemma similarity metric. We evaluate our techniques on a dataset of helper assertions we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 50% of the required helper assertions given only a few attempts, making LLMs a usable and affordable tool to further automate practical program verification.
• Abstract（参考訳）: Dafnyは人気のある検証言語で、SMTソルバにアウトソーシングすることで証明を自動化する。 しかし、この自動化は完璧ではないため、解決者はしばしば、証明エンジニアの負担を生み出すヘルパーアサーションの形でガイダンスを必要とする。 本稿では,大規模な言語モデル(LLM)を用いて,Dafnyプログラムのヘルパーアサーションを自動的に生成するツールであるLaurillを提案する。 本課題では,LLMの成功率を向上させるために,ドメイン固有の2つのプロンプト手法を設計する。 まず、検証者のエラーメッセージを解析し、その位置でアサーションプレースホルダーを挿入することで、LLMがアサーションの場所を決定するのを手助けする。 第二に、私たちはLLMに同じコードベースからの例のアサーションを提供し、新しいレムマ類似度メトリックに基づいて選択します。 実世界の3つのDafnyコードベースから抽出したヘルパーアサーションのデータセットを用いて,我々の技術を評価する。 評価の結果,数回の試行で必要なヘルパーアサーションの50%以上をローレルが生成できることがわかった。

関連論文リスト

• ASSERTIFY: Utilizing Large Language Models to Generate Assertions for Production Code [0.7973214627863593]
  プロダクションアサーションは、開発者がコードに関する仮定を検証するのを助けるために、コードに埋め込まれたステートメントである。 静的解析やディープラーニングのような現在のアサーション生成技術は、プロダクションアサーションの生成に関して不足している。 このプレプリントは、LLM(Large Language Models)を活用した自動エンドツーエンドツールであるAssertifyを導入し、エンジニアリングにプロダクションアサーションを生成することで、ギャップに対処する。
  論文  参考訳（メタデータ） (2024-11-25T20:52:28Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• Are you still on track!? Catching LLM Task Drift with Activations [55.75645403965326]
  タスクドリフトは攻撃者がデータを流出させたり、LLMの出力に影響を与えたりすることを可能にする。 そこで, 簡易線形分類器は, 分布外テストセット上で, ほぼ完全なLOC AUCでドリフトを検出することができることを示す。 このアプローチは、プロンプトインジェクション、ジェイルブレイク、悪意のある指示など、目に見えないタスクドメインに対して驚くほどうまく一般化する。
  論文  参考訳（メタデータ） (2024-06-02T16:53:21Z)
• Why and When LLM-Based Assistants Can Go Wrong: Investigating the Effectiveness of Prompt-Based Interactions for Software Help-Seeking [5.755004576310333]
  大規模言語モデル(LLM)アシスタントは、ユーザーがソフトウェアをナビゲートするための検索方法の潜在的な代替手段として登場した。 LLMアシスタントは、ドメイン固有のテキスト、ソフトウェアマニュアル、コードリポジトリからの膨大なトレーニングデータを使用して、人間のようなインタラクションを模倣する。
  論文  参考訳（メタデータ） (2024-02-12T19:49:58Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [65.18096363216574]
  大規模言語モデル(LLM)は、現実世界の知識に対する推論の基礎となる必要がある。 マルチステップ推論問題におけるツールの実行には,微調整LDMエージェントの課題が残されている。 マルチステップ推論におけるツールの活用方法として, LLM の新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-01-30T21:53:30Z)
• Leveraging Large Language Models to Boost Dafny's Developers Productivity [49.64902130083662]
  本稿では、Dafny開発者の生産性を高めるために、LLM(Large Language Models)を活用することを提案する。 新しいDafnyプラグインは、Dafnyが発見および使用できない関連する補題の提案を生成する。 自動的に証明できない補題に対して、プラグインはまた、付随する計算的証明を提供しようとする。
  論文  参考訳（メタデータ） (2024-01-01T21:58:13Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

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

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