Fugu-MT 論文翻訳(概要): SLICE: Specification-Level Isolation of Contract Enforcement

論文の概要: SLICE: Specification-Level Isolation of Contract Enforcement

arxiv url: http://arxiv.org/abs/2608.21483v1
Date: Fri, 21 Aug 2026 09:49:23 GMT
ステータス: 翻訳完了
システム内更新日: 2026-08-25 13:29:43.211058
Title: SLICE: Specification-Level Isolation of Contract Enforcement
Title（参考訳）: SLICE: 契約執行の仕様レベル分離
Abstract要約: プログラミングの問題は通常、関数が実行するべき計算と、その入力が満たさなければならない条件の両方を規定する。既存のコード生成方法は、入力契約と機能要件の両方を識別する生成プロセスを提供していません。 SLICEは、要求を識別し、別々の生成段階を通してそれらに対処する生成フレームワークである。
参考スコア（独自算出の注目度）: 8.91169891688064
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract: Programming problems commonly specify both the computation a function should perform and the conditions that its inputs must satisfy. Large language models are widely used to generate code from these problem specifications, and the generated function must implement the required computation while enforcing the stated input conditions. The stated input conditions collectively form an input contract. Enforcing this contract is difficult: incomplete enforcement accepts inputs that should be rejected, whereas overly restrictive enforcement rejects inputs that should be accepted. Existing code generation methods do not provide a generation process that identifies both the input contract and the functional requirements and generates code that satisfies them jointly. We therefore introduce SLICE, a generation framework that identifies both requirements and addresses them through separate generation stages. SLICE consists of three stages: (i) Graph-based specification structuring, which grounds contract conditions to description segments in a specification graph and removes contract-only segments to form a functional view; (ii) Functional body generation, which produces multiple candidate function bodies through greedy and sampled decoding, ranks them using execution scores, and resolves ties using difference-region log probabilities; and (iii) Contract assertion generation, which generates input-validation assertions from the identified contract conditions and attaches them to the selected function body. We evaluate SLICE on ContractEval across four LLMs and compare it with six competing methods. Relative to the strongest evaluated baseline for each model, SLICE improves performance in generating code that satisfies both the functional requirements and the input contract by an average of 6.58%. Our code is available at https://github.com/suhanmen/SLICE.
Abstract（参考訳）: プログラミングの問題は通常、関数が実行するべき計算と、その入力が満たさなければならない条件の両方を規定する。大規模言語モデルはこれらの問題仕様からコードを生成するために広く使われており、生成された関数は入力条件を強制しながら必要な計算を実装しなければならない。記載された入力条件は、総合的に入力契約を形成する。不完全な執行は拒否されるべき入力を受け入れるが、過度に制限された執行は受け入れるべき入力を拒絶する。既存のコード生成方法は、入力契約と機能要件の両方を識別し、それらを共同で満足するコードを生成する生成プロセスを提供していません。したがって、SLICEは、要求を識別し、別々の生成段階を通してそれらに対処する生成フレームワークである。 SLICEは3つのステージから構成される。一仕様グラフにおける記述セグメントに契約条件を基礎とし、機能的なビューを形成するために契約のみのセグメントを除去するグラフベースの仕様構成二グリージー及びサンプルデコードにより複数の候補機能体を生成する機能体生成であって、実行スコアを用いてランク付けし、差分領域ログの確率を用いて関係を解消すること。三特定された契約条件から入値アサーションを生成し、選択された機能体にアサーションする契約アサーション生成。本研究では,4つのLLM間でのContractEval上でのSLICEを評価し,競合する6つの手法と比較する。各モデルで最も評価されたベースラインに対して、SLICEは、機能要件と入力契約の両方を満たすコードを生成する際のパフォーマンスを平均6.58%向上させる。私たちのコードはhttps://github.com/suhanmen/SLICE.comで公開されています。

関連論文リスト

SpecCoder: Specification-Aware Code Generation with Curriculum Dual-Task Reinforcement Learning [30.588079618949447]
SpecCoderは、コード生成のための2段階のトレーニングフレームワークである。まず、GRPを訓練し、構造化された仕様分析を導出し、それらに条件付きコードを生成する。このカリキュラムは仕様誘導生成と識別を共同で最適化し、仕様とコード動作のより強力な対応を促進する。
論文参考訳（メタデータ） (2026-09-05T11:52:54Z)
VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文参考訳（メタデータ） (2026-06-03T20:02:35Z)
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文参考訳（メタデータ） (2026-02-10T06:58:26Z)
Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? [1.9551668880584971]
大規模言語モデル(LLM)は、自然言語のヒントから正式な後条件を推測する際の約束を示す。 NL2Contractは,非公式な自然言語を形式的関数型コントラクトに変換するためにLLMを使用するタスクである。 NL2Contract with different LLMs and compared it to the task of postcondition generation nl2postcond。
論文参考訳（メタデータ） (2025-10-14T16:37:39Z)
Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
論文参考訳（メタデータ） (2025-10-14T01:12:37Z)
A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design [0.16921396880325779]
私たちはDesign by Contractの原則を適用して、すべての大規模言語モデルの呼び出しを仲介するコントラクトを導入します。契約満足度は確率的であり、セマンティックな検証は運用上定義されます。この研究は、同一の契約を満たす2つのエージェントがそれらの契約に対して機能的に等価であると仮定する。
論文参考訳（メタデータ） (2025-08-05T17:24:50Z)
IFEvalCode: Controlled Code Generation [69.28317223249358]
本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
論文参考訳（メタデータ） (2025-07-30T08:08:48Z)
Type-Constrained Code Generation with Language Models [51.03439021895432]
本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
論文参考訳（メタデータ） (2025-04-12T15:03:00Z)
SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
論文参考訳（メタデータ） (2025-03-03T01:55:20Z)
ArchCode: Incorporating Software Requirements in Code Generation with Large Language Models [20.105490443135675]
ARCHCODEは、記述中の要求を整理し、表現されていない要求を外挿するフレームワークである。 ARCHCODEは所定の記述から要求を生成し、コードスニペットとテストケースを生成するように条件付けする。パブリックベンチマークによると、ARCHCODEは機能要件を満たすために拡張され、Pass@kスコアが大幅に改善されている。
論文参考訳（メタデータ） (2024-08-02T03:54:36Z)
Lexically-constrained Text Generation through Commonsense Knowledge Extraction and Injection [62.071938098215085]
我々は、ある入力概念のセットに対して妥当な文を生成することを目的としているcommongenベンチマークに焦点を当てる。生成したテキストの意味的正しさを高めるための戦略を提案する。
論文参考訳（メタデータ） (2020-12-19T23:23:40Z)

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

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