Fugu-MT 論文翻訳(概要): Lemur: Integrating Large Language Models in Automated Program Verification

論文の概要: 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 Large Language Model Aided Program Refinement [10.089955747110444]
プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。 LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
論文参考訳（メタデータ） (2024-06-26T04:29:27Z)
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 [85.3879908356586]
タスク自動化における大規模言語モデルの能力を評価するためにTaskBenchを導入します。高品質な評価データセットを生成するために,ツールグラフの概念を導入する。また,タスク分解,ツールの実行,パラメータ予測など,さまざまな側面からLCMの能力を評価するためのTaskEvalを提案する。
論文参考訳（メタデータ） (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)
SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文参考訳（メタデータ） (2023-05-16T17:55:51Z)
AutoPrompt: Eliciting Knowledge from Language Models with Automatically Generated Prompts [46.03503882865222]
AutoPromptは、勾配誘導検索に基づいて、さまざまなタスクセットのプロンプトを作成する自動メソッドである。マスク付き言語モデル(MLM)は,感情分析や自然言語推論を,追加パラメータや微調整を伴わずに行う能力を持つことを示す。
論文参考訳（メタデータ） (2020-10-29T22:54:00Z)

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