論文の概要: Intent-aligned Formal Specification Synthesis via Traceable Refinement
- arxiv url: http://arxiv.org/abs/2604.10392v1
- Date: Sun, 12 Apr 2026 00:52:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-14 20:13:15.989851
- Title: Intent-aligned Formal Specification Synthesis via Traceable Refinement
- Title（参考訳）: トレーサブルリファインメントによるインテントアライン形式仕様合成
- Abstract要約: VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。
VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。
我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
- 参考スコア（独自算出の注目度）: 43.72968325799861
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models are increasingly used to generate code from natural language, but ensuring correctness remains challenging. Formal verification offers a principled way to obtain such guarantees by proving that a program satisfies a formal specification. However, specifications are frequently missing in real-world codebases, and writing high-quality specifications remains expensive and expertise-intensive. We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair. VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps to validate generated specifications. When validation fails, traceability maps attribute failures to specific requirements, enabling targeted clause-level repairs. VeriSpecGen achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales. Beyond inference-time gains, we generate 343K training examples from VeriSpecGen refinement trajectories and demonstrate that training on these trajectories substantially improves specification synthesis by 62-106% relative and transfers gains to general reasoning abilities.
- Abstract（参考訳）: 大きな言語モデルは、自然言語からコードを生成するためにますます使われていますが、正確性を保証することは依然として困難です。
形式検証は、プログラムが形式仕様を満たすことを証明することによって、そのような保証を得るための原則化された方法を提供する。
しかし、現実世界のコードベースでは仕様が欠落することが多く、高品質な仕様を書くことは高価で専門知識に重点を置いている。
VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。
VeriSpecGenは、自然言語をアトミックな要件に分解し、明確なトレーサビリティマップで要求対象のテストを生成して、生成された仕様を検証する。
検証が失敗した場合、トレーサビリティーは障害を特定の要件にマッピングし、ターゲットの節レベルの修復を可能にする。
VeriSpecGen は Claude Opus 4.5 を使用して VERINA SpecGen タスクで 86.6% を達成した。
推論時間ゲインの他に、VeriSpecGen精錬軌道から343Kのトレーニング例を生成し、これらのトラジェクトリのトレーニングが62-106%の相対的な仕様合成を著しく改善し、一般的な推論能力にゲインを移すことを実証した。
関連論文リスト
- IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。
提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。
IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
論文 参考訳（メタデータ） (2026-09-09T17:59:04Z) - How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
Coinsは、信頼できるテストケースの評価下で仕様をインスタンス化し、具体的な証明義務を生成することで仕様品質を評価する評価フレームワークである。
我々はHumanEvalに関する大規模な研究を、人間によるRocq仕様のキュレートされたセットで実施する。
以上の結果から, 仕様生成は依然として重大な課題であり, 検証の複雑さは仕様品質の真の相違を曖昧にする可能性があることが示唆された。
論文 参考訳（メタデータ） (2026-08-13T10:45:18Z) - Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。
SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
論文 参考訳（メタデータ） (2026-07-05T11:09:30Z) - SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
我々は、プロバイダが承認したモデル仕様を主アライメントターゲットとして扱う新しいアライメントパラダイムである仕様基底アライメントを提案する。
仕様文書から直接アライメントデータを合成するフレームワークであるSpecAlignを紹介する。
論文 参考訳（メタデータ） (2026-06-15T06:30:52Z) - VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation [2.2194977808724405]
大規模言語モデルは自然言語から有用なコードを生成することができるが、その出力は正確性を保証することなく得られる。
検証可能なコード生成は、モデルに実行可能なコードだけでなく、正式な仕様やマシンチェック可能な証明を生成することを要求することによって、テストを越える道を提供する。
We present VeriContest, a benchmark of 946 competitive-playming problem from LeetCode and Codeforces for verible code generation in Rust with Verus。
論文 参考訳（メタデータ） (2026-05-08T23:25:05Z) - From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。
NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。
7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。
以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
論文 参考訳（メタデータ） (2026-04-24T14:28:10Z) - SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification [10.586396714718457]
SpecSyn は LLM ベースの新しい仕様生成手法である。
実験では、SpecSynは90%以上の高精度なリコールと75%以上の卓越したリコールを維持している。
さらなる評価では、SpecSynは1365のターゲットプロパティのうち1071の処理に成功している。
論文 参考訳（メタデータ） (2026-04-23T11:46:19Z) - CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。
CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。
リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
論文 参考訳（メタデータ） (2026-04-14T04:31:45Z) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。
プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。
また, GPT-4o miniが74.18%と高い修理成功率を示した。
論文 参考訳（メタデータ） (2025-07-04T15:36:12Z) - VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。
LLM生成コードの正確性を保証することは依然として困難である。
検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
論文 参考訳（メタデータ） (2025-05-29T06:12:52Z) - SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。
SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
論文 参考訳（メタデータ） (2024-01-16T20:13:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。