論文の概要: Teaching Code LLMs to Reason with Intermediate Formal Specifications
- arxiv url: http://arxiv.org/abs/2607.04232v1
- Date: Sun, 05 Jul 2026 11:09:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-07 22:26:29.871521
- Title: Teaching Code LLMs to Reason with Intermediate Formal Specifications
- Title（参考訳）: 中間形式仕様で推論するコードLLM
- Authors: Minh Le-Anh, Cuong Chi Le, Tien N. Nguyen,
- Abstract要約: SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。
SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
- 参考スコア（独自算出の注目度）: 9.552020178028576
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.
- Abstract（参考訳）: 自然言語仕様とは異なり、実行可能な形式仕様は、コードの検証、デバッグ、修復のためのマシンチェック可能な制約を提供する。
しかし、そのような仕様を書くことは労働集約的であり、既存のLCMベースの手法は主にプログラム全体の事前/事後条件を推論し、プログラマがアルゴリズムを推論する際に依存する中間的な意味的コミットメントを欠いている。
さらに、現在のCodeLLMは、構文的に無効で、自明で、動作を変える欠陥を否定するには弱すぎる、実行可能なアサーションをしばしば生成することを示す。
本稿では,アサーションを有意な内部プログラムポイントに挿入し,期待する中間状態を記述した実行可能なチェックポイント仕様生成について検討する。
検証誘導型CodeLLMトレーニングフレームワークであるSpecCoderを導入し、検証された参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学習する。
SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
この設定を評価するために、最近のCodeforcesの競合プログラミング問題とテストスイート、参照ソリューション、ヒューマンバギーな提案から構築されたベンチマークであるHumanExecを紹介し、仕様生成、プログラムの正当性チェック、プログラム修復の3つのタスクをサポートする。
HumanExecの実験では、SpecCoderはベースコードLLMよりもチェックポイント特定品質を大幅に改善している。
Qwen2.5-Coderモデル全体で、SpecCoderはインライン特定精度を最大55.8%改善し、完全性は最大358.1%向上し、実行可能アサーション妥当性は最大26.6%向上した。
これらの利得は、下流の正当性推論と修復にさらに寄与し、実行可能チェックポイントが信頼性のある検証のためのきめ細かい証拠を提供することを示した。
関連論文リスト
- 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) - POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference [10.01438318022033]
実世界のソフトウェアからメソッドレベルの後条件生成を評価するベンチマークであるPOSTCONDBENCHを紹介する。
自動評価を可能にするため、POSTCONDBENCHは実行可能な実行環境を提供し、欠陥識別を通じて完全性を運用する。
以上の結果から,リポジトリレベルの依存関係とメソッドの複雑性が,このギャップを悪化させることを示す。
論文 参考訳（メタデータ） (2026-05-05T04:29:38Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。
CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。
リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
論文 参考訳（メタデータ） (2026-04-14T04:31:45Z) - VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
自動JML仕様合成における古典的手法と急進的手法を比較した。
提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。
本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
論文 参考訳（メタデータ） (2026-03-31T22:12:15Z) - VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
我々は,Large Language Models (LLM) の形式的検証のための新しいベンチマークを導入する。
筆者らのフレームワークは, 基調整合を定式化された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。
以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。
論文 参考訳（メタデータ） (2025-10-07T13:19:05Z) - From Benchmark Data To Applicable Program Repair: An Experience Report [1.6913109767046948]
本稿では,プログラムの自動修復へのアプローチについて述べる。
我々はこの目的を達成するために文学の様々な技法を組み合わせている。
実験の結果,我々の手法は標準ベンチマークの他の手法よりも優れていることがわかった。
綿密な検査では、これらのテクニックはいずれも、業界で見られる現実的な欠陥には効かない。
論文 参考訳（メタデータ） (2025-08-22T03:59:27Z) - IFEvalCode: Controlled Code Generation [69.28317223249358]
本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。
IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
論文 参考訳（メタデータ） (2025-07-30T08:08:48Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。