論文の概要: Further Progress Towards Operation Proof Obligation Generation for VDM

• arxiv url: http://arxiv.org/abs/2608.19848v1
• Date: Thu, 20 Aug 2026 09:50:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-21 20:28:51.525774
• Title: Further Progress Towards Operation Proof Obligation Generation for VDM
• Title（参考訳）: VDMの運用義務化に向けたさらなる進展
• Abstract要約: VDM形式は、モデルの内部的一貫性を保証する。潜在的な矛盾は、証明義務と呼ばれる主張によって強調される。 本稿では,VDM 操作の証明義務生成について,[1] で記述した作業の更新について述べる。
• 参考スコア（独自算出の注目度）: 0.21847754147782886
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The VDM formalism can ensure that models are internally consistent. Potential inconsistencies are highlighted by assertions called proof obligations. This paper is an update to the work described in [1], regarding proof obligation generation for VDM operations. We present the latest work which improves the approach to loop invariants, adds loop variants, improves proof obligations for operation calls, including implicitly declared operations and specification statements, and adds recursive measures for operations. The new features are illustrated with examples.
• Abstract（参考訳）: VDM形式は、モデルを内部的に一貫することを保証する。 潜在的な矛盾は証明義務と呼ばれる主張によって強調される。 本稿では,VDM 操作の証明義務生成について,[1] で記述した作業の更新について述べる。 本稿では,ループ不変性に対するアプローチの改善,ループ不変性の追加,暗黙的に宣言された操作や仕様文を含む操作呼び出しの証明義務の改善,操作に対する再帰的措置の追加などについて述べる。 新機能を例に挙げる。

関連論文リスト

• Variational Learning for Insertion-based Generation [50.15012125719375]
  可変長挿入モデルの挿入順序を学習するための確率的フレームワークを提案する。 本稿では,挿入する場所,挿入する場所,終了するタイミングを共同で学習する生成モデルであるInsertion Process (IP)を提案する。
  論文  参考訳（メタデータ） (2026-06-01T11:59:46Z)
• ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
  大規模言語モデル(LLM)のための逆例誘導フレームワークであるEXVERUSを提案する。 証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。 評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。
  論文  参考訳（メタデータ） (2026-03-26T18:14:34Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。 我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。 我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-13T01:33:20Z)
• Edit-Based Flow Matching for Temporal Point Processes [51.33476564706644]
  時間的ポイントプロセス(TPP)は、イベントシーケンスを連続的にモデル化するための基本的なツールである。 最近の非自己回帰拡散型モデルでは、ノイズとデータとの連立補間によってこれらの問題を緩和している。 本稿では,TPPの編集操作を挿入,削除,置換することで,ノイズをデータに転送する編集フロープロセスを提案する。
  論文  参考訳（メタデータ） (2025-10-07T15:44:12Z)
• Towards Operation Proof Obligation Generation for VDM [0.0]
  義務の生成は、メソッドをサポートするツールの重要な役割である。 この作業では、この問題に対処するための現在の作業状況を説明し、これまでの能力を示し、残りの作業を強調します。
  論文  参考訳（メタデータ） (2025-06-15T14:18:17Z)
• Leveraging LLM Inconsistency to Boost Pass@k Performance [3.797421474324735]
  大規模言語モデル(LLM)は、多くのドメインにおいて印象的な能力を発揮するが、マイナーな入力変更に対する不整合性を示す。 本稿では,Pass@kの性能向上にモデルの不整合を利用した新しい手法を提案する。 具体的には、与えられたタスクのk変種を生成し、各タスクに対して1つの候補解を提出する「変数」エージェントを提案する。
  論文  参考訳（メタデータ） (2025-05-19T10:22:04Z)
• Steering LLMs for Formal Theorem Proving [1.083373217040891]
  我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。 このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。 1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
  論文  参考訳（メタデータ） (2025-02-21T15:04:48Z)
• Dual Conditional Diffusion Models for Sequential Recommendation [63.82152785755723]
  シーケンスレコメンデーションのための二重条件拡散モデル(DCRec)を提案する。 DCRecは2つの条件を前と逆の拡散プロセスに埋め込むことで暗黙的および明示的な情報を統合する。 これによってモデルは、明示的なユーザ-イテムインタラクションを活用してレコメンデーションプロセスをガイドしながら、価値あるシーケンシャルおよびコンテキスト情報を保持することができる。
  論文  参考訳（メタデータ） (2024-10-29T11:51:06Z)
• Fine-Tuning on Diverse Reasoning Chains Drives Within-Inference CoT Refinement in LLMs [63.36637269634553]
  本稿では,LLMを微調整し,一つの推論ステップで思考の逆連鎖(DCoT)を生成する手法を提案する。 DCoTの微調整により,モデルファミリおよびスケール間のCoTベースライン上での性能が向上することを示す。 我々の研究は、定量的解析と手動評価の両方で、観測された利益は、最初の推論連鎖を洗練させるモデルの能力に由来することを明らかにしているため、重要である。
  論文  参考訳（メタデータ） (2024-07-03T15:01:18Z)
• Code Models are Zero-shot Precondition Reasoners [83.8561159080672]
  シーケンシャルな意思決定タスクのために、コード表現を使ってアクションの前提条件を推論します。 本稿では,政策によって予測される行動が前提条件と一致していることを保証する事前条件対応行動サンプリング戦略を提案する。
  論文  参考訳（メタデータ） (2023-11-16T06:19:27Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。 RABは両方の制限を解除することで既存のモデルを一般化する。 データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-08-12T17:03:50Z)
• Invertible DenseNets with Concatenated LipSwish [8.315801422499861]
  Invertible Dense Networks (i-DenseNets) をResidual Flowsのより効率的な代替品として紹介する。 本稿では,モデルが生成モデルと識別モデルの両方を持つハイブリッドモデルとして訓練された場合,提案モデルが残留流れより優れていることを示す。
  論文  参考訳（メタデータ） (2021-02-04T15:45:33Z)

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

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