論文の概要: Lemur: Integrating Large Language Models in Automated Program Verification

• arxiv url: http://arxiv.org/abs/2310.04870v3
• Date: Sun, 24 Mar 2024 18:10:03 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-27 02:57:27.895421
• Title: Lemur: Integrating Large Language Models in Automated Program Verification
• Title（参考訳）: Lemur: プログラムの自動検証に大規模言語モデルを統合する
• Authors: Haoze Wu, Clark Barrett, Nina Narodytska,
• Abstract要約: 自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。 計算を音響自動検証の手順としてインスタンス化し、一連の合成および競合ベンチマークを実践的に改善した。
• 参考スコア（独自算出の注目度）: 10.221822902660458
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of derivation rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure, which led to practical improvements on a set of synthetic and competition benchmarks.
• Abstract（参考訳）: LLMの実証されたコード理解能力は、検証ツールで難しいプログラムプロパティに関する高度な抽象的推論を必要とするタスクである自動プログラム検証に使用できるかどうかという問題を提起する。 自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。 我々は、この方法論を導出規則の集合として公式に記述し、その健全性を証明する。 計算を音響自動検証の手順としてインスタンス化し、一連の合成および競合ベンチマークを実践的に改善した。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• LLM can Achieve Self-Regulation via Hyperparameter Aware Generation [88.69052513433603]
  大規模言語モデル (LLM) は、生成されたテキストを制御するために様々な復号法を用いる。 LLMはこれらのデコード戦略の存在を意識し、自己統制できるのか? ハイパーパラメータ・アウェア・ジェネレーション(HAG)と呼ばれる新しいテキスト生成パラダイムを提案する。
  論文  参考訳（メタデータ） (2024-02-17T11:18:22Z)
• Counting Reward Automata: Sample Efficient Reinforcement Learning Through the Exploitation of Reward Function Structure [13.231546105751015]
  本稿では,形式言語として表現可能な任意の報酬関数をモデル化可能な有限状態機械変種であるカウント・リワード・オートマトンを提案する。 このような抽象機械を組み込んだエージェントが,現在の手法よりも大きなタスクの集合を解くことができることを実証する。
  論文  参考訳（メタデータ） (2023-12-18T17:20:38Z)
• TaskBench: Benchmarking Large Language Models for Task Automation [82.2932794189585]
  タスク自動化における大規模言語モデル(LLM)の機能を評価するためのフレームワークであるTaskBenchを紹介する。 具体的には、タスクの分解、ツールの選択、パラメータ予測を評価する。 提案手法は, 自動構築と厳密な人的検証を組み合わせることで, 人的評価との整合性を確保する。
  論文  参考訳（メタデータ） (2023-11-30T18:02:44Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• AutoPrompt: Eliciting Knowledge from Language Models with Automatically Generated Prompts [46.03503882865222]
  AutoPromptは、勾配誘導検索に基づいて、さまざまなタスクセットのプロンプトを作成する自動メソッドである。 マスク付き言語モデル(MLM)は,感情分析や自然言語推論を,追加パラメータや微調整を伴わずに行う能力を持つことを示す。
  論文  参考訳（メタデータ） (2020-10-29T22:54:00Z)

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

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