論文の概要: AutoVerus: Automated Proof Generation for Rust Code

• arxiv url: http://arxiv.org/abs/2409.13082v1
• Date: Thu, 19 Sep 2024 20:40:52 GMT
• ステータス: 処理完了
• システム内更新日: 2024-11-07 12:03:17.513934
• Title: AutoVerus: Automated Proof Generation for Rust Code
• Title（参考訳）: AutoVerus: Rustコードの自動証明生成
• Authors: Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu,
• Abstract要約: AutoVerusは大規模な言語モデル(LLM)を使用して、Rustコードの正確性証明を自動的に生成する。 評価の結果,AutoVerusは90%以上の正解を自動生成できることがわかった。
• 参考スコア（独自算出の注目度）: 25.56534570237484
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLM to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.
• Abstract（参考訳）: 生成AIは多くのソフトウェアエンジニアリングタスクに対してその価値を示してきた。 いまだに、LLMベースの大規模言語モデル(LLM)ベースの証明生成は、LLMベースのコード生成に遅れを取っている。 本稿ではAutoVerusについて述べる。 AutoVerusはLLMを使用して、Rustコードの正当性証明を自動的に生成する。 AutoVerusは、Rustで書かれた証明と仕様を使って、Rustコードの正しさを証明できる検証ツールであるVerusのユニークな機能と一致するように設計されている。 AutoVerusは、人間の専門家による3つの証明構築のフェーズを模倣して構築され、編成されたLCMエージェントのネットワークで構成されている。 AutoVerusを徹底的に評価し、この方向への今後の研究を促進するために、既存のコード生成ベンチマークと検証ベンチマークに基づいて、150の非自明な証明タスクからなるベンチマークスイートを構築しました。 評価の結果,AutoVerusは90%以上の正解を自動生成し,その半数以上が30秒未満か3回のLDMコールで処理可能であることがわかった。

関連論文リスト

• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Generating Unseen Code Tests In Infinitum [1.0674604700001968]
  本稿では,プログラミングタスクやプログラミング言語にまたがって一般化するベンチマークのバリエーションを作成する手法を提案する。 我々は、Pythonでテキストからコードを生成するタスクに対して、textitauto-regressionと呼ばれる1つのベンチマークを実装した。
  論文  参考訳（メタデータ） (2024-07-29T08:11:20Z)
• AutoDetect: Towards a Unified Framework for Automated Weakness Detection in Large Language Models [95.09157454599605]
  大規模言語モデル(LLM)はますます強力になってきていますが、それでも顕著ですが微妙な弱点があります。 従来のベンチマークアプローチでは、特定のモデルの欠陥を徹底的に特定することはできない。 さまざまなタスクにまたがるLLMの弱点を自動的に露呈する統合フレームワークであるAutoDetectを導入する。
  論文  参考訳（メタデータ） (2024-06-24T15:16:45Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。 その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
  論文  参考訳（メタデータ） (2024-06-16T21:11:23Z)
• Laurel: Generating Dafny Assertions Using Large Language Models [2.6942525604796366]
  本稿では,大規模な言語モデル(LLM)を用いて,Dafnyプログラムのヘルパーアサーションを自動的に生成するツールであるLaurillを提案する。 Laurelは数回の試行で、必要なヘルパーアサーションの50%以上を生成することができる。
  論文  参考訳（メタデータ） (2024-05-27T03:26:01Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Teaching Large Language Models to Self-Debug [62.424077000154945]
  大規模言語モデル(LLM)は、コード生成において素晴らしいパフォーマンスを達成した。 本稿では,大規模言語モデルで予測プログラムを数発のデモでデバッグする自己デバッグを提案する。
  論文  参考訳（メタデータ） (2023-04-11T10:43:43Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• ReCode: Robustness Evaluation of Code Generation Models [90.10436771217243]
  コード生成モデルのための総合的ロバストネス評価ベンチマークであるReCodeを提案する。 ドクストリング、関数と変数名、コード構文、コードフォーマットのコードに特化して、30以上の変換をカスタマイズします。 ヒトのアノテータでは、摂動プロンプトの90%以上が本来のプロンプトの意味を変えていないことが確認された。
  論文  参考訳（メタデータ） (2022-12-20T14:11:31Z)

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

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