論文の概要: VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
- arxiv url: http://arxiv.org/abs/2510.25015v1
- Date: Tue, 28 Oct 2025 22:28:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-30 15:50:44.812849
- Title: VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
- Title（参考訳）: VeriStruct:Verusにおけるデータ構造モジュールの自動検証
- Authors: Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett,
- Abstract要約: We introduced VeriStruct, a framework that a AI-assisted verification from single function to more complex data structure module in Verus。
11つのRustデータ構造モジュールの評価において、VeriStructは11つ中10つで成功し、合計で129の関数(99.2%)のうち128つを検証できた。
- 参考スコア（独自算出の注目度）: 3.660044314479077
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification.
- Abstract（参考訳）: VeriStructは、単一の関数からより複雑なデータ構造モジュールへのAI支援自動検証を拡張する新しいフレームワークである。
VeriStructは、抽象化、型不変性、仕様、証明コードの体系的な生成をオーケストレーションするために、プランナーモジュールを使用している。
LLMがVerusのアノテーション構文と検証固有のセマンティクスを誤解することが多い問題に対処するため、VeriStructはプロンプト内に構文ガイダンスを組み込み、自動的にアノテーションエラーを修正するための修正段階を含む。
11つのRustデータ構造モジュールの評価において、VeriStructは11つ中10つで成功し、合計で129の関数(99.2%)のうち128つを検証できた。
これらの結果は、自動AI支援形式検証の目標に向けた重要なステップである。
関連論文リスト
- Dissect-and-Restore: AI-based Code Verification with Transient Refactoring [1.2883590530210827]
提案するPrometheusは,現在のAI機能を備えた自動コード検証を容易にする,AI支援システムである。
プロメテウスは、複素補題の構造的分解を通じてより小さく検証可能な部分補題への証明探索を導く。
このアプローチは、ベースラインの68%に比べて、キュレートされたデータセットの86%のタスクをうまく検証します。
論文 参考訳（メタデータ） (2025-10-29T11:23:50Z) - Structure-R1: Dynamically Leveraging Structural Knowledge in LLM Reasoning through Reinforcement Learning [29.722512436773638]
本稿では,検索したコンテンツを推論に最適化した構造化表現に変換するフレームワークであるtextscStructure-R1を提案する。
textscStructure-R1は、7Bスケールのバックボーンモデルとの競合性能を一貫して達成していることを示す。
我々の理論的分析は,情報密度と文脈的明瞭度を向上させることによって,構造化表現が推論をいかに促進するかを示す。
論文 参考訳（メタデータ） (2025-10-16T23:19:28Z) - Structured Prompting and Feedback-Guided Reasoning with LLMs for Data Interpretation [0.0]
大規模言語モデル(LLM)は、自然言語の理解とタスクの一般化において顕著な能力を示した。
本稿では、構造化されたプロンプトおよびフィードバック駆動型変換ロジック生成手法であるSTROT Frameworkを紹介する。
論文 参考訳（メタデータ） (2025-05-03T00:05:01Z) - Struct-X: Enhancing Large Language Models Reasoning with Structured Data [38.558614152006975]
構造Xは5つの重要なフェーズを通して動作する:read-model-fill-reflect-reason'
構造化データをグラフ埋め込みを用いて位相空間にエンコードする。
行方不明のエンティティ情報を知識検索モジュールで埋める。
最後のフェーズでは、選択したトークンでトポロジネットワークを構築する。
論文 参考訳（メタデータ） (2024-07-17T13:06:25Z) - StructLM: Towards Building Generalist Models for Structured Knowledge Grounding [49.10029030628653]
大規模言語モデル(LLM)では、最先端(SoTA)モデルの背後にある構造化データラグを平均35%処理できる。
私たちは、MistralとCodeLlamaモデルファミリに基づいたStructLMと呼ばれる一連のモデルをトレーニングします。
我々のStructLMシリーズは、評価された18のデータセットのうち16のタスク固有モデルを超え、8つのSKGタスクに新しいSoTAパフォーマンスを確立する。
論文 参考訳（メタデータ） (2024-02-26T15:47:01Z) - StructGPT: A General Framework for Large Language Model to Reason over
Structured Data [117.13986738340027]
我々は,構造化データに基づく質問応答タスクの解法として,emphIterative Reading-then-Reasoning(IRR)アプローチを開発した。
提案手法はChatGPTの性能を大幅に向上させ,全データの教師付きベースラインに対して同等のパフォーマンスを実現する。
論文 参考訳（メタデータ） (2023-05-16T17:45:23Z) - StrAE: Autoencoding for Pre-Trained Embeddings using Explicit Structure [5.2869308707704255]
StrAEは構造化オートエンコーダフレームワークであり、明示的な構造に厳格に固執することで、マルチレベル表現の効果的な学習を可能にする。
本研究の結果は,入力として提供される構造に直接的な関連性があることを示し,既存のツリーモデルではそうではないことを示す。
次に、StrAEを拡張して、単純なローカライズ・マージアルゴリズムを用いてモデルが独自の構成を定義する。
論文 参考訳（メタデータ） (2023-05-09T16:20:48Z) - Autoregressive Structured Prediction with Language Models [73.11519625765301]
本稿では, PLM を用いた自己回帰的手法を用いて, モデル構造を行動列として記述する。
我々のアプローチは、私たちが見てきた全ての構造化予測タスクにおいて、新しい最先端を実現する。
論文 参考訳（メタデータ） (2022-10-26T13:27:26Z) - DeepStruct: Pretraining of Language Models for Structure Prediction [64.84144849119554]
テキストから構造を生成するために,タスクに依存しないコーパスの集合上で言語モデルを事前訓練する。
我々の構造事前学習は、モデルが構造タスクについて持っている学習知識のゼロショット転送を可能にする。
10Bパラメータ言語モデルがほとんどのタスクに非自明に転送し、28のデータセットのうち21の最先端のパフォーマンスを得ることを示す。
論文 参考訳（メタデータ） (2022-05-21T00:58:22Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。