論文の概要: Automated Proof Generation for Rust Code via Self-Evolution

• arxiv url: http://arxiv.org/abs/2410.15756v1
• Date: Mon, 21 Oct 2024 08:15:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-22 13:21:43.897580
• Title: Automated Proof Generation for Rust Code via Self-Evolution
• Title（参考訳）: 自己進化によるRustコードの自動証明生成
• Authors: Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, Lidong Zhou,
• Abstract要約: 私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
• 参考スコア（独自算出の注目度）: 69.25795662658356
• License:
• Abstract: Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction and hence raises a pressing need for automation. The primary obstacle lies in the severe lack of data - there is much less proof than code for LLMs to train upon. In this paper, we introduce SAFE, a novel framework that overcomes the lack of human-written proof to enable automated proof generation of Rust code. SAFE establishes a self-evolving cycle where data synthesis and fine-tuning collaborate to enhance the model capability, leveraging the definitive power of a symbolic verifier in telling correct proof from incorrect ones. SAFE also re-purposes the large number of synthesized incorrect proofs to train the self-debugging capability of the fine-tuned models, empowering them to fix incorrect proofs based on the verifier's feedback. SAFE demonstrates superior efficiency and precision compared to GPT-4o. Through tens of thousands of synthesized proofs and the self-debugging mechanism, we improve the capability of open-source models, initially unacquainted with formal verification, to automatically write proof for Rust code. This advancement leads to a significant improvement in performance, achieving a 70.50% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 24.46%.
• Abstract（参考訳）: コード生成には正確性を保証することが重要です。 形式的検証は、確実な正当性の保証を提供するが、立証に相当な人的努力を要するため、自動化の必要性が高まっている。 一番の障害はデータの不足です - LLMがトレーニングするコードよりもはるかに少ないコードです。 本稿では,Rustコードの自動証明生成を実現するために,人による証明の欠如を克服する新しいフレームワークであるSAFEを紹介する。 SAFEは、データ合成と微調整が協調してモデル能力を高める自己進化サイクルを確立し、正しい証明を誤ったものとするために記号検証器の決定的な力を利用する。 SAFEはまた、多数の合成された不正確な証明を再利用し、細調整されたモデルの自己デバッグ能力を訓練し、検証者のフィードバックに基づいて不正な証明を修正する権限を与える。 SAFEはGPT-4oに比べて効率と精度が優れている。 何万もの合成証明と自己デバッグメカニズムを通じて、私たちは、Rustコードの証明を自動記述するために、最初は正式な検証を知らなかったオープンソースのモデルの性能を改善しました。 この進歩は、人間の専門家によるベンチマークで70.50%の精度で性能が向上し、GPT-4oのパフォーマンスが24.46%を上回った。

関連論文リスト

• AutoVerus: Automated Proof Generation for Rust Code [25.56534570237484]
  AutoVerusは大規模な言語モデル(LLM)を使用して、Rustコードの正確性証明を自動的に生成する。 評価の結果,AutoVerusは90%以上の正解を自動生成できることがわかった。
  論文  参考訳（メタデータ） (2024-09-19T20:40:52Z)
• Synchronous Faithfulness Monitoring for Trustworthy Retrieval-Augmented Generation [96.78845113346809]
  Retrieval-augmented Language Model (RALMs) は、知識集約型タスクにおいて、高い性能と幅広い適用性を示している。 本稿では,非偽文の検出に微細な復号力学を利用する軽量モニタであるSynCheckを提案する。 また、長文検索拡張生成のためのビームサーチによって導かれる忠実度指向の復号アルゴリズムであるFODを導入する。
  論文  参考訳（メタデータ） (2024-06-19T16:42:57Z)
• Model Reprogramming Outperforms Fine-tuning on Out-of-distribution Data in Text-Image Encoders [56.47577824219207]
  本稿では,侵入的微調整技術に関連する隠れたコストを明らかにする。 ファインチューニングのための新しいモデル再プログラミング手法を導入し、それをリプログラマと呼ぶ。 我々の経験的証拠は、Re Programmerは侵入力が少なく、より優れた下流モデルが得られることを示している。
  論文  参考訳（メタデータ） (2024-03-16T04:19:48Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• Certified Adversarial Defenses Meet Out-of-Distribution Corruptions: Benchmarking Robustness and Simple Baselines [65.0803400763215]
  この研究は、最先端のロバストモデルがアウト・オブ・ディストリビューションデータに遭遇した場合、敵のロバスト性がどのように変化を保証しているかを批判的に検証する。 本稿では,トレーニングデータのスペクトルカバレッジを改善するために,新たなデータ拡張方式であるFourierMixを提案する。 また,FourierMixの拡張により,様々なOODベンチマークにおいて,より優れたロバスト性保証を実現することが可能となる。
  論文  参考訳（メタデータ） (2021-12-01T17:11:22Z)
• Security and Privacy Enhanced Gait Authentication with Random Representation Learning and Digital Lockers [3.3549957463189095]
  慣性センサーによってキャプチャされた歩行データは、ユーザ認証において有望な結果を示している。 既存のほとんどのアプローチでは、登録された歩行パターンをパターンと一致させるために安全に保存しているため、重要なセキュリティとプライバシの問題が発生している。 本稿では,歩行データからユーザ認証のためのランダムキーを生成するゲイト暗号システムを提案する。
  論文  参考訳（メタデータ） (2021-08-05T06:34:42Z)
• Zero-shot Fact Verification by Claim Generation [85.27523983027471]
  我々は,堅牢な事実検証モデルをトレーニングするフレームワークであるQACGを開発した。 われわれは自動的に生成されたクレームを使って、Wikipediaのエビデンスからサポートしたり、反論したり、検証したりできる。 ゼロショットシナリオでは、QACGはRoBERTaモデルのF1を50%から77%に改善し、パフォーマンスは2K以上の手作業による例に相当する。
  論文  参考訳（メタデータ） (2021-05-31T03:13:52Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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