論文の概要: 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（参考訳）: 運動の機械的およびエージェント的仕様推論
- 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コードのコーパスに適用されている。
関連論文リスト
- Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳（メタデータ） (2026-08-04T13:01:30Z) - Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
我々は、プロバイダが承認したモデル仕様を主アライメントターゲットとして扱う新しいアライメントパラダイムである仕様基底アライメントを提案する。
仕様文書から直接アライメントデータを合成するフレームワークであるSpecAlignを紹介する。
論文 参考訳（メタデータ） (2026-06-15T06:30:52Z) - Agentic Separation Logic Specification Synthesis [4.177196802192322]
Spec-Agentは、大規模なC++で表現力のある、よく検証された仕様を合成するためのエージェントシステムである。
それぞれの関数に対して、Spec-Agentは静的解析とランタイムヒープトレースを使用して、適切なターゲット仕様言語を選択する。
数百万行のコードからなるオープンソースのC++上でSpec-Agentを評価する。
論文 参考訳（メタデータ） (2026-05-26T18:05:42Z) - Agentic Model Checking [12.832868209928039]
本稿では,LLMエージェントと境界モデルチェックバックエンドを結合するパラダイムを提案する。
我々は、BMC-Agentのアプローチをインスタンス化し、CとRustのLLM生成カーネルおよびコンパイラコード上で評価する。
論文 参考訳（メタデータ） (2026-05-20T17:25:52Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。