論文の概要: ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis

• arxiv url: http://arxiv.org/abs/2512.10173v1
• Date: Thu, 11 Dec 2025 00:21:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-12 16:15:42.128396
• Title: ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
• Title（参考訳）: ATLAS: 大規模検証コード合成のための自動ツールキット
• Authors: Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Soonho Kong,
• Abstract要約: ATLASは仕様、実装、証明を備えた完全なDafnyプログラムを生成する。 プログラム1つにつき7つ以上の学習例を, 合成過程を特殊タスクに分解して抽出する。
• 参考スコア（独自算出の注目度）: 0.4908879620102719
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models have shown potential for program verification, but progress is hindered by the scarcity of verified code for training. We present ATLAS, an automated pipeline that synthesizes verified programs at scale to address this data bottleneck. ATLAS generates complete Dafny programs with specifications, implementations, and proofs, producing 2.7K verified programs from which we extract over 19K training examples--more than 7 per verified program--by decomposing the synthesis process into multiple specialized tasks. Fine-tuning Qwen 2.5 7B Coder on this dataset produces substantial gains: +23 percentage points on DafnyBench and +50 percentage points on DafnySynthesis. These results demonstrate that synthetic verified code can effectively enhance LLM capabilities for formal verification.
• Abstract（参考訳）: 大規模言語モデルは、プログラム検証の可能性を示しているが、訓練のための検証コードの不足によって進歩が妨げられている。 我々は、このデータボトルネックに対処するために、検証済みプログラムを大規模に合成する自動パイプラインATLASを提案する。 ATLASは、仕様、実装、証明を備えた完全なDafnyプログラムを生成し、2.7K以上の検証済みプログラムを生成します。 このデータセット上の微調整 Qwen 2.5 7B コーダは、DafnyBench の +23 %、DafnySynthesis の +50 % の大幅な増加をもたらす。 これらの結果から, 合成検証符号は, 形式検証のためのLLM能力を効果的に向上できることが示された。

関連論文リスト

• Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning [7.574481956683386]
  この研究は、新しいエンドツーエンド合成フレームワークであるProof2Siliconを提示する。 以前提案されたPreFACEフローを組み込んで、自然言語仕様から直接、正確性バイコンストラクションハードウェアを生成する。
  論文  参考訳（メタデータ） (2025-09-07T23:04:15Z)
• UnitCoder: Scalable Iterative Code Synthesis with Unit Test Guidance [65.01483640267885]
  大きな言語モデル(LLM)は、様々なタスクにおいて顕著な能力を示してきたが、コード生成は依然として大きな課題である。 私たちは、モデル生成ユニットテストを活用してコード生成プロセスのガイドと検証を行う、システマティックパイプラインであるUnitCoderを紹介します。 我々の研究は、モデル生成単体テストを利用して、事前学習コーパスから高品質なコードデータの合成を誘導するスケーラブルなアプローチを提案する。
  論文  参考訳（メタデータ） (2025-02-17T05:37:02Z)
• Genetic Instruct: Scaling up Synthetic Generation of Coding Instructions for Large Language Models [59.60208063956459]
  大規模言語モデル(LLM)は、効果的なアライメントのために高品質な命令データを必要とする。 本稿では,大規模かつ高品質な符号化命令を合成するスケーラブルなアルゴリズムであるGenematic-Instructを提案する。
  論文  参考訳（メタデータ） (2024-07-29T20:42:59Z)
• Case2Code: Scalable Synthetic Data for Code Generation [105.89741089673575]
  大規模言語モデル(LLM)は、コード生成において顕著なブレークスルーを示している。 最近の研究は、いくつかの強力なLLMによって生成された合成データをトレーニングすることで、コードLLMを改善している。 プログラムの表現性と正確性を利用したtextbfCase2Code タスクを提案する。
  論文  参考訳（メタデータ） (2024-07-17T11:35:00Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• TarGEN: Targeted Data Generation with Large Language Models [51.87504111286201]
  TarGENは、高品質な合成データセットを生成するための、多段階のプロンプト戦略である。 我々は,LLMが不正確なラベル付きインスタンスを修正できるようにする自己補正法により,TarGENを増強する。 合成データセットを元のデータセットと比較した包括的な分析により、データセットの複雑さと多様性の類似または高いレベルが明らかになる。
  論文  参考訳（メタデータ） (2023-10-27T03:32:17Z)
• The Program Testing Ability of Large Language Models for Code [27.590499335039972]
  CodeXやCodeT5+のようなコードのための大きな言語モデル(LLM)は、コードインテリジェンスを達成する上で大きな可能性を実証しています。 本稿では、これらのモデルの興味深い特性のシリーズを示し、LLMのプログラムテスト能力をいかに改善できるかを示す。
  論文  参考訳（メタデータ） (2023-10-09T13:55:45Z)

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

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