論文の概要: Lemur: Integrating Large Language Models in Automated Program Verification
- arxiv url: http://arxiv.org/abs/2310.04870v5
- Date: Thu, 25 Apr 2024 01:16:21 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-26 23:47:37.531309
- 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 transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.
- Abstract(参考訳): LLMの実証されたコード理解能力は、検証ツールで難しいプログラムプロパティに関する高度な抽象的推論を必要とするタスクである自動プログラム検証に使用できるかどうかという問題を提起する。
自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。
我々は、この方法論をトランジションルールの集合として公式に記述し、その健全性を証明する。
本稿では,音声自動検証手法として計算をインスタンス化し,一連の合成および競合ベンチマークの実践的改善を実証する。
関連論文リスト
- Towards Generating Executable Metamorphic Relations Using Large Language
Models [49.632090604977364]
大規模言語モデル(LLM)を用いた要件から実行可能なMRを自動的に抽出する手法を提案する。
提案手法の有効性を評価するため,シーメンス・インダストリー・ソフトウェアと共同で質問紙調査を行った。
論文 参考訳(メタデータ) (2024-01-30T13:52:47Z) - 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 [85.3879908356586]
タスク自動化における大規模言語モデルの能力を評価するためにTaskBenchを導入します。
高品質な評価データセットを生成するために,ツールグラフの概念を導入する。
また,タスク分解,ツールの実行,パラメータ予測など,さまざまな側面からLCMの能力を評価するためのTaskEvalを提案する。
論文 参考訳(メタデータ) (2023-11-30T18:02:44Z) - CLOMO: Counterfactual Logical Modification with Large Language Models [113.72984199026094]
本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。
生成モデルのカウンターファクトの能力を効果的に評価するために,革新的な評価指標であるLogicAware Counterfactual Scoreを提案する。
分析の結果,提案手法は人間の好みとよく一致していることがわかった。
論文 参考訳(メタデータ) (2023-11-29T08:29:54Z) - Automatic Program Instrumentation for Automatic Verification (Extended
Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。
本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。
我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文 参考訳(メタデータ) (2023-05-26T14:55:35Z) - SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。
我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。
我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文 参考訳(メタデータ) (2023-05-16T17:55:51Z) - Inverse Reinforcement Learning of Autonomous Behaviors Encoded as
Weighted Finite Automata [18.972270182221262]
本稿では,論理タスク仕様とコスト関数を実演から学習する手法を提案する。
本稿では,タスクの未知論理構造を近似した重み付き有限オートマトン(WFA)の抽出にスペクトル学習手法を用いる。
高レベルタスクガイダンスのためのWFAと低レベル制御のためのラベル付きマルコフ決定プロセス(L-MDP)との間にある製品を定義し、実証者の行動にマッチするコスト関数を最適化する。
論文 参考訳(メタデータ) (2021-03-10T06:42:10Z) - AutoPrompt: Eliciting Knowledge from Language Models with Automatically
Generated Prompts [46.03503882865222]
AutoPromptは、勾配誘導検索に基づいて、さまざまなタスクセットのプロンプトを作成する自動メソッドである。
マスク付き言語モデル(MLM)は,感情分析や自然言語推論を,追加パラメータや微調整を伴わずに行う能力を持つことを示す。
論文 参考訳(メタデータ) (2020-10-29T22:54:00Z) - Induction and Exploitation of Subgoal Automata for Reinforcement
Learning [75.55324974788475]
本稿では,Regressed Learning (RL)タスクにおけるサブゴールの学習と活用のためのISAを提案する。
ISAは、タスクのサブゴールによってエッジがラベル付けされたオートマトンであるサブゴールオートマトンを誘導することで強化学習をインターリーブする。
サブゴールオートマトンはまた、タスクの完了を示す状態と、タスクが成功せずに完了したことを示す状態の2つの特別な状態で構成されている。
論文 参考訳(メタデータ) (2020-09-08T16:42:55Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。