論文の概要: Leveraging Large Language Models for Automated Proof Synthesis in Rust
- arxiv url: http://arxiv.org/abs/2311.03739v2
- Date: Wed, 22 Nov 2023 23:49:03 GMT
- ステータス: 処理完了
- システム内更新日: 2023-11-28 02:39:45.281341
- Title: Leveraging Large Language Models for Automated Proof Synthesis in Rust
- Title(参考訳): rustの自動証明合成に大規模な言語モデルを活用する
- Authors: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
- Abstract要約: 大規模言語モデル(LLM)は、コード解析と合成に成功している。
我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。
プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
- 参考スコア(独自算出の注目度): 6.202137610101939
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal verification can provably guarantee the correctness of critical system
software, but the high proof burden has long hindered its wide adoption.
Recently, Large Language Models (LLMs) have shown success in code analysis and
synthesis. In this paper, we present a combination of LLMs and static analysis
to synthesize invariants, assertions, and other proof structures for a
Rust-based formal verification framework called Verus. In a few-shot setting,
LLMs demonstrate impressive logical ability in generating postconditions and
loop invariants, especially when analyzing short code snippets. However, LLMs
lack the ability to retain and propagate context information, a strength of
traditional static analysis. Based on these observations, we developed a
prototype based on OpenAI's GPT-4 model. Our prototype decomposes the
verification task into multiple smaller ones, iteratively queries GPT-4, and
combines its output with lightweight static analysis. We evaluated the
prototype with a developer in the automation loop on 20 vector-manipulating
programs. The results demonstrate that it significantly reduces human effort in
writing entry-level proof code.
- Abstract(参考訳): 形式的検証は、重要なシステムソフトウェアの正しさを確実に保証するが、高い証明負担が長い間その普及を妨げてきた。
近年,大規模言語モデル(llm)がコード解析と合成に成功している。
本稿では,LLMと静的解析を組み合わせることで,Rustベースの公式検証フレームワークVerusの不変性,アサーション,その他の証明構造を合成する。
数ショット設定では、llmはポストコンディションの生成やループ不変量、特に短いコードスニペットの解析において印象的な論理能力を示している。
しかし、LLMには従来の静的解析の強みである文脈情報を保持・伝播する能力がない。
これらの観測に基づいて,OpenAIのGPT-4モデルに基づくプロトタイプを開発した。
プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,出力と軽量な静的解析を組み合わせる。
20個のベクタ操作プログラムの自動化ループにおいて,プロトタイプを開発者によって評価した。
結果は、エントリレベルの証明コードを記述する人の労力を大幅に削減できることを示しています。
関連論文リスト
- MiniCheck: Efficient Fact-Checking of LLMs on Grounding Documents [62.02920842630234]
GPT-4レベルの性能を持つ小型モデルを400倍のコストで構築する方法を示す。
既存のデータセットを LLM-AggreFact ベンチマークにまとめる。
我々の最良のシステム MiniCheck-FT5 (770Mパラメータ) は、同等の大きさの全てのシステムより優れ、GPT-4精度に達する。
論文 参考訳(メタデータ) (2024-04-16T17:59:10Z) - Perplexed: Understanding When Large Language Models are Confused [3.4208414448496027]
本稿では,言語モデルが複雑になる場所を探索するライブラリであるperplexedを紹介する。
Codetokenizerと呼ばれるコードモデルの解析を支援するために構築した追加ツールを使用して、コード生成のためのLLM(Large Language Models)に焦点を当てたケーススタディを実施しました。
我々の研究したコードLLMは、コードが構文的に正しくないコーディング構造において、最悪のパフォーマンスを示しました。
論文 参考訳(メタデータ) (2024-04-09T22:03:39Z) - E&V: Prompting Large Language Models to Perform Static Analysis by
Pseudo-code Execution and Verification [7.745665775992235]
大きな言語モデル(LLM)は、ソフトウェア工学のタスクに新しい機能を提供する。
LLMは擬似コードの実行をシミュレートし、最小限の努力で擬似コードにエンコードされた静的解析を効果的に実行する。
E&Vは、外部のオラクルを必要とせずに擬似コード実行の検証プロセスを含む。
論文 参考訳(メタデータ) (2023-12-13T19:31:00Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳(メタデータ) (2023-10-23T17:58:40Z) - Evaluating and Explaining Large Language Models for Code Using Syntactic
Structures [74.93762031957883]
本稿では,コード用大規模言語モデルに特有の説明可能性手法であるASTxplainerを紹介する。
その中核にあるASTxplainerは、トークン予測をASTノードに整合させる自動メソッドを提供する。
私たちは、最も人気のあるGitHubプロジェクトのキュレートデータセットを使用して、コード用の12の人気のあるLLMに対して、実証的な評価を行います。
論文 参考訳(メタデータ) (2023-08-07T18:50:57Z) - The Hitchhiker's Guide to Program Analysis: A Journey with Large
Language Models [18.026567399243]
大規模言語モデル(LLM)は静的解析に代わる有望な選択肢を提供する。
本稿では,LLM支援静的解析のオープン空間を深く掘り下げる。
LLiftは,静的解析ツールとLLMの両方を併用した,完全に自動化されたフレームワークである。
論文 参考訳(メタデータ) (2023-08-01T02:57:43Z) - Large Language Models as General Pattern Machines [64.75501424160748]
我々は,事前訓練された大規模言語モデル (LLM) が,複雑なトークンシーケンスを自動回帰的に完了することを示す。
驚いたことに、語彙からランダムにサンプリングされたトークンを用いてシーケンスが表現された場合でも、パターン完了の習熟度を部分的に保持することができる。
本研究では,ロボット工学における問題に対して,これらのゼロショット機能がどのように適用されるかを検討する。
論文 参考訳(メタデータ) (2023-07-10T17:32:13Z) - Explaining Emergent In-Context Learning as Kernel Regression [61.57151500616111]
大規模言語モデル(LLM)は、伝達学習のパラダイムシフトを開始した。
本稿では,トランスフォーマーに基づく言語モデルが事前学習後に文脈内学習を達成できる理由について検討する。
ICL中、LLMの注意と隠れた特徴は、カーネル回帰の挙動と一致していることがわかった。
論文 参考訳(メタデータ) (2023-05-22T06:45:02Z) - Benchmarking Large Language Models for Automated Verilog RTL Code
Generation [21.747037230069854]
有用なVerilogを生成するために,大規模言語モデル(LLM)を特徴付ける。
機能解析のためのテストベンチと,Verilogコードの構文をテストするフローからなる評価フレームワークを構築した。
その結果,LLMの微調整結果は,構文的に正しいコードを生成する能力が高いことがわかった。
論文 参考訳(メタデータ) (2022-12-13T16:34:39Z) - Language Models Are Greedy Reasoners: A Systematic Formal Analysis of
Chain-of-Thought [10.524051272257614]
大規模言語モデル(LLM)は、チェーン・オブ・シークレット・プロンプトが与えられた顕著な推論能力を示している。
本稿では, PrOntoQAと呼ばれる合成質問応答データセットを提案し, それぞれの例を合成世界モデルとして生成する。
これにより、生成された連鎖を形式解析の象徴的な証明に解析することができる。
論文 参考訳(メタデータ) (2022-10-03T21:34:32Z) - Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。
既存のアプローチは、ログ特化や手動ルール抽出に依存している。
本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文 参考訳(メタデータ) (2020-03-17T19:25:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。