論文の概要: Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

• arxiv url: http://arxiv.org/abs/2602.04910v1
• Date: Wed, 04 Feb 2026 01:04:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-06 18:49:08.532745
• Title: Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
• Title（参考訳）: シードトレーニングセットのスケールアップによるラストシステムにおける証明合成コストの削減
• Authors: Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R. Lorch, Yuan Yao, Xiaoxing Ma,
• Abstract要約: 本稿では,Rustで記述されたシステムソフトウェアの検証ツールであるVerusのデータ合成パイプラインであるVeruSynを紹介する。 690万のRustプログラムで、それぞれが正式な仕様と、それがその仕様を満たしている証拠を持って、最大のVerus検証プログラムを合成します。 このデータセットによって、コスト対効果の高いトレードオフを備えた微調整のQwen2.5-Coder-32B-Instructモデルが作成できます。
• 参考スコア（独自算出の注目度）: 40.85677634306877
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to have LLMs generate formal correctness proofs along with such code. However, compared with code generation, code-proof generation requires much higher reasoning capability and has much less existing data to learn from. In this paper, we present VeruSyn, a data synthesis pipeline for Verus, a state-of-the-art verification tool for system software written in Rust. Through self-synthesis and tutorial-based synthesis, VeruSyn achieves much larger scale and Verus-feature coverage than previous data-synthesis techniques designed for Verus; VeruSyn also supplements its dataset with long-chain-of-thought (CoT) data through agent trajectory synthesis. With VeruSyn, we synthesize the largest set of Verus verified programs: 6.9 million Rust programs, each with a formal specification and a proof that it meets that specification. This dataset lets us create a fine-tuned Qwen2.5-Coder-32B-Instruct model with appealing cost-proof tradeoff compared with state-of-the-art commercial models like Claude Sonnet 4.5. It also significantly outperforms models like o4-mini and previously proposed research models.
• Abstract（参考訳）: 大規模言語モデル(LLM)はコード生成に広く使われている。 しかし、LLMが生成したコードの正確性は依然として懸念されている。 この懸念に対する潜在的対策は、LSMがそのようなコードとともに正式な正当性証明を生成することである。 しかし、コード生成と比較して、コード保護生成は推論能力がはるかに高く、そこから学ぶべき既存のデータが少ない。 本稿では,Rustで記述されたシステムソフトウェアのための最先端の検証ツールであるVerusのデータ合成パイプラインであるVeruSynを紹介する。 自己合成とチュートリアルベースの合成を通じて、VeruSynは、従来のVerus用に設計されたデータ合成技術よりもはるかに大きなスケールとVerus-Featureカバレッジを実現している。 VeruSynでは690万のRustプログラムという,最大の検証プログラムセットを合成しています。 このデータセットは、Claude Sonnet 4.5のような最先端の商用モデルと比較して、コスト対効果の高いトレードオフを備えた微調整のQwen2.5-Coder-32B-Instructモデルを作成することができます。 また、o4-miniや以前に提案された研究モデルなどのモデルも大幅に上回っている。

関連論文リスト

• Limited Preference Data? Learning Better Reward Model with Latent Space Synthesis [19.056892622506826]
  リワードモデリングは、大きな言語モデルと人間の嗜好の整合に不可欠である。 既存のテキストデータ合成手法は計算コストが高い。 本稿では,言語に潜む埋め込み空間において,好みデータを直接合成するための新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-09-30T10:48:50Z)
• Scaling Laws of Synthetic Data for Language Models [125.41600201811417]
  プレトレーニングコーパスを多種多様な高品質な合成データセットに変換するスケーラブルなフレームワークであるSynthLLMを紹介した。 提案手法は,グラフアルゴリズムを用いて複数の文書にまたがるハイレベルな概念を自動的に抽出し,再結合することで実現している。
  論文  参考訳（メタデータ） (2025-03-25T11:07:12Z)
• UnitCoder: Scalable Iterative Code Synthesis with Unit Test Guidance [65.01483640267885]
  大きな言語モデル(LLM)は、様々なタスクにおいて顕著な能力を示してきたが、コード生成は依然として大きな課題である。 私たちは、モデル生成ユニットテストを活用してコード生成プロセスのガイドと検証を行う、システマティックパイプラインであるUnitCoderを紹介します。 我々の研究は、モデル生成単体テストを利用して、事前学習コーパスから高品質なコードデータの合成を誘導するスケーラブルなアプローチを提案する。
  論文  参考訳（メタデータ） (2025-02-17T05:37:02Z)
• Training Language Models on Synthetic Edit Sequences Improves Code Synthesis [33.13471417703669]
  言語モデル(LM)はプログラムを1回のパスで自動的に合成する。 コード合成のための高品質な命令データが不足している一方で、合成のための編集データが不足している。 我々はこのギャップを埋めるためにLintSeqと呼ばれる合成データ生成アルゴリズムを開発した。
  論文  参考訳（メタデータ） (2024-10-03T17:57:22Z)
• SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
  トピック分類,感情分析,トーン検出,ユーモアの6つのデータセットの合成について検討した。 その結果,SynthesizRRは語彙や意味の多様性,人文との類似性,蒸留性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-05-16T12:22:41Z)

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

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