論文の概要: Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification

• arxiv url: http://arxiv.org/abs/2609.34886v1
• Date: Mon, 28 Sep 2026 10:58:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-03 01:58:10.182997
• Title: Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification
• Title（参考訳）: 設計による推測の少ない: LLM支援動詞検証のための再利用可能なスキル
• Abstract要約: 慎重に設計された検証技術を備えたLLMエージェントは,VerusのDLLに対して,強力かつ低信頼な仕様を作成可能であることを示す。 慎重に設計された検証技術を備えたLLMエージェントは,VerusのDLLに対して,強力かつ低信頼な仕様を作成可能であることを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for verification—it becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.
• Abstract（参考訳）: LLM支援のVerus検証は、Rustの実装を検証するための退屈な方法ではありませんが、例えば、DLL(Doubly Linked Lists)など、自己参照構造と組み合わせることによって、検証の形式化が困難であることは、極めて要求の多い検証タスクになります。 さらに、検証が公理的補題や前提文のような証明されていない仮定や無効化された仮定に依存すると、仕様の弱点が生じる。 LLMエージェントがこれらの信頼基盤を最小化しつつ、強力なDLL仕様を合成できるかどうかを検討する。 この分析は、手動検証、プロパティ固有の検証、DLLの特定のケースとこの種のデータ構造の特定の特性について定義されたスキルの3つの異なるアプローチに従っている。 スキルはドメイン知識とタスク分割戦略をエンコードする。 慎重に設計された検証技術を備えたLLMエージェントは,Verus における DLL の信頼性の高い低信頼仕様を生成することができることを示す。

関連論文リスト

• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。 NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。 7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。 以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
  論文  参考訳（メタデータ） (2026-04-24T14:28:10Z)
• Trust but Verify: Introducing DAVinCI -- A Framework for Dual Attribution and Verification in Claim Inference for Language Models [53.279391576560755]
  大規模言語モデル(LLM)は、広範囲のNLPタスクにおいて顕著な流速と汎用性を示してきたが、実際的な不正確さと制限が伴う傾向にある。 これは、信頼と妥当性が最優先される医療、法律、科学コミュニケーションといった、高リスク領域に重大なリスクをもたらす。 LLM出力の事実的信頼性と解釈可能性を高めるために設計されたDAVinCI - Dual Attribution and Verificationフレームワークを紹介する。
  論文  参考訳（メタデータ） (2026-04-23T01:37:50Z)
• Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought [1.167370706056905]
  VCoT-Liftは低レベルの解法推論を高レベルで可読性のある検証ステップに引き上げる。 VCoT-Benchは、欠落した証明の様々な程度に対する堅牢性、異なる証明タイプに対する能力、証明位置に対する感度の3つの次元で性能を測定する。
  論文  参考訳（メタデータ） (2026-03-18T22:42:20Z)
• Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
  我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。 より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。 そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
  論文  参考訳（メタデータ） (2026-02-28T08:35:25Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  データ駆動の不確実性スコアに基づくステップレベルの推論検証の軽量な代替案を提案する。 本研究は, LLMの内部状態が不確実性を符号化し, 信頼性の高い検証信号として機能することが示唆された。
  論文  参考訳（メタデータ） (2025-11-09T03:38:29Z)
• LLMs as verification oracles for Solidity [1.3887048755037537]
  本稿では,この役割において,最先端の推論LLMである GPT-5 を初めて体系的に評価する。 我々は,大規模な検証タスクのデータセット上でその性能をベンチマークし,その出力を確立された形式的検証ツールと比較し,実世界の監査シナリオにおける実効性を評価する。 我々の研究は、AIの収束における新たなフロンティアと、セキュアなスマートコントラクト開発と監査のための形式的手法を示唆している。
  論文  参考訳（メタデータ） (2025-09-23T15:32:13Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Reasoning-CV: Fine-tuning Powerful Reasoning LLMs for Knowledge-Assisted Claim Verification [17.35114345065597]
  CoT(Chain-of-Thought)-Verifyパラダイムは、サブステートへの分解を必要とせず、検証段階を分離することなく、元の複雑クレームに対するCoT検証パスを生成する。 Reasoning-CVは既存のDecompose-Then-Verify法よりも優れた知識支援クレーム検証性能を示す。
  論文  参考訳（メタデータ） (2025-05-18T10:28:54Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。 11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。 最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
  論文  参考訳（メタデータ） (2024-07-23T15:31:26Z)

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

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