論文の概要: VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners

• arxiv url: http://arxiv.org/abs/2404.18852v2
• Date: Sat, 25 May 2024 15:15:12 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-29 05:47:26.242399
• Title: VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners
• Title（参考訳）: VERT: 大きな言語モデルによる検証された等価なRustトランスパイラ
• Authors: Aidan Z. H. Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, Daniel Kroening,
• Abstract要約: Rustはメモリ安全性と低レベルのコントロールを組み合わせたプログラミング言語で、Cライクなパフォーマンスを提供する。 既存の作業はルールベースと大規模言語モデル(LLM)という2つのカテゴリに分類される。 私たちは、正式な正確性を保証する形で、可読性のあるRustトランスパイルを生成するツールであるVERTを紹介します。
• 参考スコア（独自算出の注目度）: 6.824327908701066
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Rust is a programming language that combines memory safety and low-level control, providing C-like performance while guaranteeing the absence of undefined behaviors by default. Rust's growing popularity has prompted research on safe and correct transpiling of existing code-bases to Rust. Existing work falls into two categories: rule-based and large language model (LLM)-based. While rule-based approaches can theoretically produce correct transpilations that maintain input-output equivalence to the original, they often yield unreadable Rust code that uses unsafe subsets of the Rust language. On the other hand, while LLM-based approaches typically produce more readable, maintainable, and safe code, they do not provide any guarantees about correctness. In this work, we present VERT, a tool that can produce readable Rust transpilations with formal guarantees of correctness. VERT's only requirement is that there is Web Assembly compiler for the source language, which is true for most major languages. VERT first uses the Web Assembly compiler to obtain an oracle Rust program. In parallel, VERT uses an LLM to generate a readable candidate Rust program. This candidate is verified against the oracle, and if verification fails, we regenerate a new candidate transpilation until verification succeeds. We evaluate VERT by transpiling a suite of 1,394 programs taken from competitive programming style benchmarks. Combining Anthropic's Claude-2 and VERT increases Rust transpilations passing property-based testing from 31% to 54% and bounded model-checking from 1% to 42% compared to using Claude alone. In addition, we evaluate VERT's ability to generate non-trivial safe Rust on programs taken from real-world C projects that make significant use of pointers. Our results provide insights into the limitations of LLMs to write safe Rust.
• Abstract（参考訳）: Rustはメモリ安全性と低レベルのコントロールを組み合わせたプログラミング言語で、デフォルトでは未定義の動作がないことを保証しながら、Cライクなパフォーマンスを提供する。 Rustの人気が高まっているため、既存のコードベースをRustに安全かつ正しく移行する研究が進められている。 既存の作業はルールベースと大規模言語モデル(LLM)という2つのカテゴリに分類される。 ルールベースのアプローチは理論上、インプット・アウトプットの等価性をオリジナルに維持する正しいトランスパイルを生成することができるが、多くの場合、Rust言語の安全でないサブセットを使用する可読性のないRustコードを生成する。 一方、LLMベースのアプローチは一般的により読みやすく、保守性があり、安全なコードを生成するが、正確性に関する保証は提供しない。 本研究では,可読性のあるRustトランスパイルを,正式な正確性を保証するツールであるVERTを紹介する。 VERTの唯一の要件は、ソース言語にWebアセンブリコンパイラが存在することだ。 VERTはまず、Web Assemblyコンパイラを使用して、オラクルRustプログラムを取得する。 並行して、VERTはLLMを使用して読み取り可能な候補Rustプログラムを生成する。 この候補はオラクルに対して検証され、検証が失敗した場合、検証が成功するまで新しい候補の複製を再生する。 我々は、競合プログラミングスタイルのベンチマークから得られた1,394個のプログラムをトランスパイルすることで、VERTを評価する。 AnthropicのClaude-2とVERTを組み合わせることで、プロパティベースのテストに合格するRustのトランスパイルが31%から54%に増加し、モデルチェックのバウンドが1%から42%に増加した。 さらに、ポインタを多用する現実世界のCプロジェクトから取得したプログラムに対して、VERTが非自明な安全なRustを生成する能力を評価した。 我々の結果は、安全なRustを書くためのLLMの制限に関する洞察を与えてくれます。

関連論文リスト

• Context-aware Code Segmentation for C-to-Rust Translation using Large Language Models [1.8416014644193066]
  大きな言語モデル(LLM)は、ルールベースのメソッドよりも自然で安全なコードを生成することで、この翻訳を自動化することを約束している。 大規模Cコードをコンパイル可能なRustコードに変換する際の成功率を改善するLLMベースの翻訳方式を提案する。 4キロのコードを含む20のベンチマークCプログラムの実験では、すべてのプログラムをコンパイル可能なRustコードに変換することに成功した。
  論文  参考訳（メタデータ） (2024-09-16T17:52:36Z)
• CRUXEval-X: A Benchmark for Multilingual Code Reasoning, Understanding and Execution [50.7413285637879]
  CRUXEVAL-Xコード推論ベンチマークには19のプログラミング言語が含まれている。 各言語に対して少なくとも600人の被験者で構成され、合計19Kのコンテンツ一貫性テストがある。 Pythonでのみトレーニングされたモデルでさえ、他の言語で34.4%のPass@1を達成することができる。
  論文  参考訳（メタデータ） (2024-08-23T11:43:00Z)
• Investigating the Transferability of Code Repair for Low-Resource Programming Languages [57.62712191540067]
  大規模言語モデル(LLM)は、コード生成タスクにおいて顕著なパフォーマンスを示している。 近年の作業は、連鎖推論や蒸留といった現代的な技術を統合することで、コード修復のプロセスを強化している。 高低資源言語と低低資源言語の両方でコード修復を蒸留する利点について検討する。
  論文  参考訳（メタデータ） (2024-06-21T05:05:39Z)
• A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries [2.359557447960552]
  Rustは、他の言語との相互運用に頻繁に使用される。 Miriは、これらのモデルに対してアプリケーションを検証できる唯一の動的解析ツールである。 Miriは外部機能をサポートしておらず、Rustエコシステムの中心に重要な正当性ギャップがあることを示唆している。
  論文  参考訳（メタデータ） (2024-04-17T18:12:05Z)
• Towards a Transpiler for C/C++ to Safer Rust [0.10993800728351737]
  RustはMozillaが開発したプログラミング言語で、パフォーマンスと安全性に重点を置いている。 既存のC++コードベースをRustに変換する方法も注目されている。
  論文  参考訳（メタデータ） (2024-01-16T10:35:59Z)
• Fast Summary-based Whole-program Analysis to Identify Unsafe Memory Accesses in Rust [23.0568924498396]
  Rustは40年以上にわたって低レベルのソフトウェアに悩まされてきたメモリ安全性問題を解決する最も有望なシステムプログラミング言語の1つである。 アンセーフなRustコードと直接リンクされたアンセーフな外部ライブラリは、メモリ安全違反自体を導入するだけでなく、セーフなRustと同じモノリシックなアドレス空間で実行されるプログラム全体を侵害する可能性がある。 我々は、安全でないヒープの割り当てと、それらの安全でないヒープオブジェクトへのメモリアクセスの両方を識別するためのプログラム全体をプロトタイプ化した。
  論文  参考訳（メタデータ） (2023-10-16T11:34:21Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Fixing Rust Compilation Errors using LLMs [2.1781086368581932]
  Rustプログラミング言語は、C/C++のような従来の安全でない代替言語よりも、低レベルのシステムプログラミング言語に実行可能な選択肢として、自らを確立している。 本稿では,Large Language Models(LLMs)の創発的機能を活用し,Rustコンパイルエラーの修正を自動的に提案するRustAssistantというツールを提案する。 RustAssistantは、人気のあるオープンソースRustリポジトリの実際のコンパイルエラーに対して、約74%の驚くべきピーク精度を達成することができる。
  論文  参考訳（メタデータ） (2023-08-09T18:30:27Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)
• Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
  7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。 英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。 このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
  論文  参考訳（メタデータ） (2021-04-15T16:08:43Z)

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

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