論文の概要: 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%以上をローレルが生成できることがわかった。

関連論文リスト

• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.4779196219827508]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• 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)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• LLMAuditor: A Framework for Auditing Large Language Models Using Human-in-the-Loop [7.77005079649294]
  有効な方法は、同じ質問の異なるバージョンを使って、大きな言語モデルを探索することである。 この監査方法を大規模に運用するには、これらのプローブを確実かつ自動的に作成するためのアプローチが必要である。 我々はLLMAuditorフレームワークを提案し、異なるLLMとHIL(Human-in-the-loop)を併用する。 このアプローチは、検証性と透明性を提供すると同時に、同じLLMへの円形依存を回避する。
  論文  参考訳（メタデータ） (2024-02-14T17:49:31Z)
• 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)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。 思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。 また,LLMにも同様な自己検証能力があることを示す。
  論文  参考訳（メタデータ） (2022-12-19T15:51:52Z)

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

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