論文の概要: 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個のベクタ操作プログラムの自動化ループにおいて,プロトタイプを開発者によって評価した。
結果は、エントリレベルの証明コードを記述する人の労力を大幅に削減できることを示しています。
関連論文リスト
- Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
大規模言語モデル(LLM)は、多くのソフトウェアエンジニアリング活動において有望であることを示している。
本稿では,分離論理に基づく仕様生成におけるOpenAIのGPTモデルの有効性について検討する。
論文 参考訳（メタデータ） (2024-11-04T17:44:11Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。
GPT-4oに比べて効率と精度が優れていた。
この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。
AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
論文 参考訳（メタデータ） (2024-06-26T14:47:28Z) - Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
大規模言語モデル(LLM)は、様々なベンチマークで人間レベルの精度に到達し、さらに超えることができるが、不正確な応答における過度な自信は、依然として十分に文書化された障害モードである。
本稿では,LLMの不確実性を測定するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2024-06-05T16:35:30Z) - MiniCheck: Efficient Fact-Checking of LLMs on Grounding Documents [62.02920842630234]
GPT-4レベルの性能を持つが400倍の低コストでファクトチェックモデルを構築する方法を示す。
GPT-4を用いて合成トレーニングデータを構築することで,現実的かつ困難な事実エラーの事例を生成する。
評価のために, ファクトチェックとグラウンドグラウンド化に関する最近の研究から得られたデータセットを, 新たなベンチマーク LLM-AggreFact に統一する。
論文 参考訳（メタデータ） (2024-04-16T17:59:10Z) - LLMDFA: Analyzing Dataflow in Code with Large Language Models [8.92611389987991]
本稿では,コンパイル不要でカスタマイズ可能なデータフロー解析フレームワークLLMDFAを提案する。
問題をいくつかのサブタスクに分解し、一連の新しい戦略を導入する。
LLMDFAは平均87.10%の精度と80.77%のリコールを達成し、F1スコアを最大0.35に向上させた。
論文 参考訳（メタデータ） (2024-02-16T15:21:35Z) - 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) - ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
本稿では,LLMベースのフレームワークであるReEvalについて述べる。
本稿では、ChatGPTを用いてReEvalを実装し、2つの人気のあるオープンドメインQAデータセットのバリエーションを評価する。
我々の生成したデータは人間可読であり、大きな言語モデルで幻覚を引き起こすのに役立ちます。
論文 参考訳（メタデータ） (2023-10-19T06:37:32Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。