論文の概要: Laurel: Unblocking Automated Verification with Large Language Models

• arxiv url: http://arxiv.org/abs/2405.16792v2
• Date: Mon, 03 Mar 2025 22:24:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-05 19:09:43.663809
• Title: Laurel: Unblocking Automated Verification with Large Language Models
• Title（参考訳）: Laurel: 大きな言語モデルで自動検証をブロックする
• Authors: Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou,
• Abstract要約: 大規模言語モデルを用いてアサーションを自動的に生成するツールであるLaurellを提案する。 実世界の3つのDafnysから抽出した複雑な補題のデータセットであるDafnyGymを、新しいベンチマークで評価した。
• 参考スコア（独自算出の注目度）: 2.6942525604796366
• License:
• Abstract: Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that alleviates this burden by automatically generating assertions using large language models (LLMs). 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 proof similarity metric. We evaluate our techniques on our new benchmark DafnyGym, a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 56.6\% of the required assertions given only a few attempts, making LLMs an affordable tool for unblocking program verifiers without human intervention.
• Abstract（参考訳）: Dafnyのようなプログラム検証器は、それらをSMTソルバにアウトソーシングすることで証明を自動化する。 しかし、この自動化は完璧ではなく、解決者はしばしばアサーションの形でヒントを必要とし、証明エンジニアに負担を与えます。 本稿では,大言語モデル(LLM)を用いてアサーションを自動的に生成することで,この負担を軽減するツールであるLaurellを提案する。 本課題では,LLMの成功率を向上させるために,ドメイン固有の2つのプロンプト手法を設計する。 まず、検証者のエラーメッセージを解析し、その位置でアサーションプレースホルダーを挿入することで、LLMがアサーションの場所を決定するのを手助けする。 第2に、LLMに同じコードベースからの例のアサーションを提供し、新しい証明類似度指標に基づいて選択する。 DafnyGymは実世界の3つのDafnyコードベースから抽出した複雑な補題のデータセットです。 評価の結果, LLM は人間の介入なしにプログラム検証をブロックするための安価なツールとなるため, 必要なアサーションの 56.6 % 以上を生成できることがわかった。

関連論文リスト

• ASSERTIFY: Utilizing Large Language Models to Generate Assertions for Production Code [0.7973214627863593]
  プロダクションアサーションは、開発者がコードに関する仮定を検証するのを助けるために、コードに埋め込まれたステートメントである。 静的解析やディープラーニングのような現在のアサーション生成技術は、プロダクションアサーションの生成に関して不足している。 このプレプリントは、LLM(Large Language Models)を活用した自動エンドツーエンドツールであるAssertifyを導入し、エンジニアリングにプロダクションアサーションを生成することで、ギャップに対処する。
  論文  参考訳（メタデータ） (2024-11-25T20:52:28Z)
• Learning to Ask: When LLM Agents Meet Unclear Instruction [55.65312637965779]
  大きな言語モデル(LLM)は、言語スキルだけでは達成不可能なタスクに対処するための外部ツールを活用することができる。 我々は、不完全な命令下でのLLMツールの使用性能を評価し、エラーパターンを分析し、Noisy ToolBenchと呼ばれる挑戦的なツール使用ベンチマークを構築した。 Ask-when-Needed (AwN) という新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-08-31T23:06:12Z)
• 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 [63.08202389132155]
  大規模言語モデル(LLM)は、現実世界の知識に対する推論の基礎となる必要がある。 マルチステップ推論問題におけるツールの実行には,微調整LDMエージェントの課題が残されている。 マルチステップ推論におけるツールの活用方法として, LLM の新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-01-30T21:53:30Z)
• 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)

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

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