論文の概要: Combining Mechanical and Agentic Specification Inference for Move
- arxiv url: http://arxiv.org/abs/2605.10005v2
- Date: Wed, 13 May 2026 02:35:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-14 17:13:58.847358
- Title: Combining Mechanical and Agentic Specification Inference for Move
- Title（参考訳）: 運動の機械的およびエージェント的仕様推論
- Authors: Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap,
- Abstract要約: 本稿では,Move Proverの仕様推論ツールについて述べる。
これは、Moveバイトコードに対する最も弱い条件分析とClaude CodeのようなエージェントコーディングCLIを組み合わせる。
このツールは標準的なMoveコードのコーパスに適用されている。
- 参考スコア（独自算出の注目度）: 2.8693521708495684
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic coding CLI such as Claude Code. Specification inference reduces the boilerplate of writing specifications in Move: in order to verify a high-level property such as a global state invariant, pre- and post-conditions for the supporting functions typically have to be written by hand, which is tedious. In our setting, a Model Context Protocol (MCP) service exposes the WP analysis and the prover itself to the coding agent. The WP analysis provides a sound, mechanical baseline for inference; the AI is used precisely where WP is weakest -- for loop invariants and high-level idiomatic specifications such as monotonicity, conservation, and structural invariants. The Move Prover serves as the oracle that decides whether the generated specs are valid, and the agent is equipped to generate proof hints and to refine the inferred specification until verification succeeds. The tool has been applied to a corpus of canonical Move code, including code that uses higher-order functions, dynamic dispatch, global state, references, and various forms of loops.
- Abstract（参考訳）: 本稿では、最弱条件(WP)解析とクロードコードのようなエージェントコーディングCLIを組み合わせたMove Proverの仕様推論ツールの早期開発について述べる。
仕様推論は、Moveにおける仕様書の定型化を減らす:グローバルな状態不変性のような高レベルなプロパティを検証するために、サポート関数の事前条件と後条件は、通常手書きで書かなければならないが、これは面倒である。
我々の設定では、モデルコンテキストプロトコル(MCP)サービスがWP分析と証明器自体を符号化エージェントに公開します。
AIは、ループ不変量やモノトニック性、保存性、構造不変量といったハイレベルな慣用仕様に対して、WPが最も弱い場所で正確に使用される。
Move Proverは、生成された仕様が有効かどうかを判断する託宣として機能し、エージェントは証明ヒントを生成し、検証が成功するまで推論された仕様を洗練する。
このツールは、高階関数、動的ディスパッチ、グローバル状態、参照、様々なループ形式を使用するコードを含む、標準的なMoveコードのコーパスに適用されている。
関連論文リスト
- DocSync: Agentic Documentation Maintenance via Critic-Guided Reflexion [0.0]
DocSyncは、ドキュメントのメンテナンスを構造的に基盤付けられた反復的な生成タスクとしてフレーム化するエージェントワークフローである。
LoRA適応小言語モデルを用いたDocSyncの資源制約実装を実証的に評価する。
このAST対応エージェントアプローチが標準エンコーダ・デコーダのベースラインを大幅に上回ることを示す。
論文 参考訳（メタデータ） (2026-05-04T02:41:33Z) - VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
自動JML仕様合成における古典的手法と急進的手法を比較した。
提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。
本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
論文 参考訳（メタデータ） (2026-03-31T22:12:15Z) - FMBench: Adaptive Large Language Model Output Formatting [49.52930069696333]
適応型マークダウン出力フォーマットのベンチマークであるFMBenchを提案する。
2つのモデルファミリーの実験は、SFTが一貫してセマンティックアライメントを改善していることを示している。
結果はまた、意味的目的と構造的目的の間に固有のトレードオフを明らかにします。
論文 参考訳（メタデータ） (2026-02-06T04:42:06Z) - AgenticTagger: Structured Item Representation for Recommendation with LLM Agents [58.12004213978182]
AgenticTagger は LLM をクエリして,項目をテキスト記述子のシーケンスで表現するフレームワークである。
アイテムコーパス内の語彙を効果的かつ効率的に基底化するために,多エージェント反射機構を設計する。
公開データとプライベートデータの実験では、AgenticTaggerがさまざまなレコメンデーションシナリオに一貫した改善をもたらしている。
論文 参考訳（メタデータ） (2026-02-05T18:01:37Z) - Finding the Translation Switch: Discovering and Exploiting the Task-Initiation Features in LLMs [69.28193153685893]
大きな言語モデル(LLM)は、タスク固有の微調整なしでも、しばしば強力な翻訳能力を示す。
このプロセスをデミスティフィケートするために、スパースオートエンコーダ(SAE)を活用し、タスク固有の特徴を特定するための新しいフレームワークを導入する。
我々の研究は、LLMの翻訳機構のコアコンポーネントをデコードするだけでなく、内部モデル機構を使用してより堅牢で効率的なモデルを作成するための青写真も提供しています。
論文 参考訳（メタデータ） (2026-01-16T06:29:07Z) - SeqPE: Transformer with Sequential Position Encoding [76.22159277300891]
SeqPEは、各$n$次元位置指数をシンボルシーケンスとして表現し、軽量なシーケンシャル位置エンコーダを用いて埋め込みを学習する。
言語モデリング、長文質問応答、および2次元画像分類による実験により、SeqPEはパープレキシティ、正確なマッチング(EM)、精度の強いベースラインを超えるだけでなく、手作業によるアーキテクチャ再設計を必要とせず、多次元入力へのシームレスな一般化を可能にする。
論文 参考訳（メタデータ） (2025-06-16T09:16:40Z) - AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL [6.062811197376495]
本稿では,仕様とRTLの両方から知識グラフ(KG)を構築する新しい手法を提案する。
仕様から初期KGを作成し、RTLコードから抽出された情報と体系的に融合し、統合された総合KGとなる。
4つの設計実験により,提案手法は従来手法よりもSVAの品質を著しく向上させることが示された。
論文 参考訳（メタデータ） (2025-03-24T21:53:37Z) - Discourse Features Enhance Detection of Document-Level Machine-Generated Content [53.41994768824785]
機械生成コンテンツは、学術プラジャリズムや誤報の拡散といった課題を提起する。
既存のMGC検出器は、しばしば表面レベルの情報のみに焦点を当て、暗黙的かつ構造的な特徴を見渡す。
これらの課題を克服するために、新しい方法論とデータセットを導入します。
論文 参考訳（メタデータ） (2024-12-17T08:47:41Z) - Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
我々はTLA+を用いて、ZooKeeperとTLCモデルチェッカーのきめ細かい挙動をモデル化し、その正確性を検証する。
複数きめの仕様を書くことは現実的な実践であり、不安定な状態空間を伴わずにモデルコードギャップに対処できることを示す。
論文 参考訳（メタデータ） (2024-09-22T02:59:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。