論文の概要: TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

• arxiv url: http://arxiv.org/abs/2610.14923v2
• Date: Thu, 15 Oct 2026 12:21:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-17 06:09:32.913401
• Title: TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents
• Title（参考訳）: TLA-Verus : LLMエージェントを用いた時間的証明法の生成と解決
• Abstract要約: VerusはRust用に構築された自動アクティブ検証ツールで、TLA+仕様の証明義務を大規模に生成する。 我々の研究は価値ある評価データセットをもたらし、Verusの定理証明における現在の世代モデル能力のマッピングに使用しています。
• 参考スコア（独自算出の注目度）: 3.18543759301646
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The TLA+ (temporal logic of actions) formal specification toolkit has seen widespread adoption in modeling modern distributed software systems including databases, storage systems, ledgers and coordination protocols. This popularity is despite its two significant limitations for software verification: Firstly, TLA+ offers no way to detect drift between software implementation and mathematical specification; secondly, TLC and TLAPS cannot provide satisfactory proofs of arbitrary temporal logic properties. We address the second limitation and take a first step towards the first by translating TLA+ specifications into Verus, an auto-active verifier built for Rust, via both a deterministic transpiler and an agentic translator. We demonstrate that our LLM-based pipeline is able to generate proof obligations from TLA+ specifications at scale, and to produce fully machine checkable proofs of both safety and liveness properties. Since temporal logic reasoning in Verus is a largely new task for LLMs, our work yields a valuable evaluation dataset, which we use to map out current generation model capabilities in Verus theorem proving.
• Abstract（参考訳）: TLA+形式仕様ツールキットは、データベース、ストレージシステム、台帳、調整プロトコルを含む現代の分散ソフトウェアシステムのモデリングにおいて広く採用されている。 第一に、TLA+は、ソフトウェア実装と数学的仕様の間のドリフトを検出する手段を提供しておらず、第二に、TLCとTLAPSは任意の時間論理特性の十分な証明を提供していない。 TLA+仕様を、決定論的トランスパイラとエージェントトランスレータの両方を通じて、Rust用に構築された自動アクティブ検証ツールであるVerusに翻訳することで、第2の制限に対処し、第1のステップに向かって第1のステップを踏み出します。 LLMをベースとしたパイプラインは,TLA+仕様から大規模に証明義務を発生し,安全性と生活性の両方の完全マシンチェック可能な証明を生成可能であることを実証する。 Verus の時間論理推論は LLM の新たなタスクであるので,我々の研究は,現在の世代モデル能力をVerus の定理証明にマップアウトするために,貴重な評価データセットを提供する。

関連論文リスト

• TRACE: Tackling Real-World Resource Assignment Problems via Agentic Heuristic Design [12.936419360138045]
  動的リソース割り当て — タスクストリームを異種処理ノードにリアルタイムに割り当てる — は、現代のコンピューティングインフラストラクチャのバックボーンである。 本稿では,進化的AHDループとエージェント知識抽出を結合したTRACEを提案する。 TRACEは、リソース割り当て問題において最先端のAHDメソッドを一貫して上回り、2%以上のオーバーヘッドで監査可能なリソースを得る。
  論文  参考訳（メタデータ） (2026-10-01T15:38:04Z)
• Can Large Language Models Implement Agent-Based Models? An ODD-based Replication Study [0.6821122205224714]
  大規模言語モデル(LLM)は、テキスト記述から非自明な実行可能なコードを合成できるようになった。 LLMは、複製、検証、検証をサポートする方法で、標準化された仕様からエージェントベースのモデルを確実に実装できますか? 制御されたODD-to-code翻訳タスクにおいて17の現代LLMを評価する。
  論文  参考訳（メタデータ） (2026-02-08T19:56:20Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• Beyond Next Token Probabilities: Learnable, Fast Detection of Hallucinations and Data Contamination on LLM Output Distributions [60.43398881149664]
  LLM出力シグナチャの効率的な符号化を訓練した軽量アテンションベースアーキテクチャであるLOS-Netを紹介する。 非常に低い検出レイテンシを維持しながら、さまざまなベンチマークやLLMで優れたパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-03-18T09:04:37Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  大規模言語モデル(LLM)は急速に進歩し、印象的な機能を示している。 In-Context Learning (ICL) など。 効率的なファインチューニング(PEFT)は、現在2つの主要な拡張方法である。 下流タスクへのLLM。 我々は、モデルが微調整なしで新しいタスクに迅速に適応できるパラダイムである参照信頼復号(RTD)を提案する。
  論文  参考訳（メタデータ） (2024-09-30T10:48:20Z)
• Get my drift? Catching LLM Task Drift with Activation Deltas [55.75645403965326]
  タスクドリフトは攻撃者がデータを流出させたり、LLMの出力に影響を与えたりすることを可能にする。 そこで, 簡易線形分類器は, 分布外テストセット上で, ほぼ完全なLOC AUCでドリフトを検出することができることを示す。 このアプローチは、プロンプトインジェクション、ジェイルブレイク、悪意のある指示など、目に見えないタスクドメインに対して驚くほどうまく一般化する。
  論文  参考訳（メタデータ） (2024-06-02T16:53:21Z)
• Validating Traces of Distributed Programs Against TLA+ Specifications [0.0]
  本稿では,分散プログラムのトレースをTLA+で記述された高レベル仕様に関連付けるためのフレームワークを提案する。 この問題は、TLCモデルチェッカーを用いて実現した制約付きモデルチェック問題に還元される。 提案手法を複数の分散プログラムに適用し,すべてのケースにおいて仕様と実装の相違を検出する。
  論文  参考訳（メタデータ） (2024-04-24T01:33:07Z)
• TAT-LLM: A Specialized Language Model for Discrete Reasoning over Tabular and Textual Data [73.29220562541204]
  我々は,言語モデル(LLM)の驚くべきパワーを活用して課題を解決することを検討する。 LLaMA2を微調整し,既存のエキスパートアノテートデータセットから自動生成したトレーニングデータを用いてTAT-LLM言語モデルを開発する。
  論文  参考訳（メタデータ） (2024-01-24T04:28:50Z)

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

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