論文の概要: ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair

• arxiv url: http://arxiv.org/abs/2602.12058v1
• Date: Thu, 12 Feb 2026 15:19:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-13 21:07:25.89155
• Title: ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
• Title（参考訳）: ModelWisdom: TLA+モデル可視化、ダイジェスト、修復のための統合ツールキット
• Authors: Zhiyong Chen, Jialun Cao, Chang Xu, Shing-Chi Cheung,
• Abstract要約: 可視化と大規模言語モデルを用いた対話型環境であるModelWisdomを提案する。 ModelWisdomは、(i)モデルビジュアライゼーション、色付き違反強調表示、TLA+コードへの遷移からのクリックスルーリンク、違反状態と壊れたプロパティのマッピング、(ii)ツリーベースの構造化とノード/エッジの折り畳みを含むグラフ最適化、(iii)モデルダイジェスト、(iii)大規模な言語モデル(LLM)を通じてサブグラフを要約し、説明し、前処理と部分的な説明を実行するモデルダイジェストを提供する。
• 参考スコア（独自算出の注目度）: 28.029008331214726
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Model checking in TLA+ provides strong correctness guarantees, yet practitioners continue to face significant challenges in interpreting counterexamples, understanding large state-transition graphs, and repairing faulty models. These difficulties stem from the limited explainability of raw model-checker output and the substantial manual effort required to trace violations back to source specifications. Although the TLA+ Toolbox includes a state diagram viewer, it offers only a static, fully expanded graph without folding, color highlighting, or semantic explanations, which limits its scalability and interpretability. We present ModelWisdom, an interactive environment that uses visualization and large language models to make TLA+ model checking more interpretable and actionable. ModelWisdom offers: (i) Model Visualization, with colorized violation highlighting, click-through links from transitions to TLA+ code, and mapping between violating states and broken properties; (ii) Graph Optimization, including tree-based structuring and node/edge folding to manage large models; (iii) Model Digest, which summarizes and explains subgraphs via large language models (LLMs) and performs preprocessing and partial explanations; and (iv) Model Repair, which extracts error information and supports iterative debugging. Together, these capabilities turn raw model-checker output into an interactive, explainable workflow, improving understanding and reducing debugging effort for nontrivial TLA+ specifications. The website to ModelWisdom is available: https://model-wisdom.pages.dev. A demonstrative video can be found at https://www.youtube.com/watch?v=plyZo30VShA.
• Abstract（参考訳）: TLA+のモデルチェックは、強い正当性を保証するが、反例の解釈、大規模な状態遷移グラフの理解、欠陥モデルの修復において、実践者は引き続き重大な課題に直面している。 これらの困難は、生のモデルチェッカー出力の限定的な説明可能性と、ソース仕様への違反の追跡に必要な相当な手作業に起因している。 TLA+ Toolboxには状態ダイアグラムビューアが含まれているが、折りたたみ、色強調表示、意味的な説明なしで、静的で完全に拡張されたグラフのみを提供しており、スケーラビリティと解釈性を制限する。 可視化と大規模言語モデルを用いた対話型環境であるModelWisdomを提案する。 ModelWisdomが提供します。 一 色付き違反強調表示、TLA+コードへの遷移からのクリックスルーリンク、違反状態と壊れた特性のマッピングを有するモデル可視化 (ii)大きなモデルを管理するためにツリーベースの構造化やノード/エッジの折り畳みを含むグラフ最適化 三 大型言語モデル(LLM)による部分グラフを要約し、説明し、前処理及び部分的説明を行うモデルダイジェスト (iv) エラー情報を抽出し、反復的なデバッグをサポートするモデル修復。 これらの機能を合わせて、生のモデルチェッカー出力をインタラクティブで説明可能なワークフローに変換し、非自明なTLA+仕様に対する理解とデバッグの労力を削減します。 ModelWisdom の Web サイトは https://model-wisdom.pages.dev にある。 デモ動画はhttps://www.youtube.com/watch? v=plyZo30VShA。

関連論文リスト

• Mantis: A Versatile Vision-Language-Action Model with Disentangled Visual Foresight [49.882469110319086]
  本稿では,DVF(Disentangled Visual Foresight)を特徴とする新しいフレームワークであるMantisを紹介する。 Mantisは、メタクエリと拡散トランスフォーマー(DiT)ヘッドを組み合わせて、バックボーンから視覚的予測を分離する。 マンティスは微調整後のLIBEROベンチマークで96.7%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-11-20T09:30:23Z)
• The Role of Exploration Modules in Small Language Models for Knowledge Graph Question Answering [19.009534602200862]
  KGに基づく質問応答におけるSLM(Small Language Model)に対する既存の統合手法の能力について検討する。 この制限に対処するため,単純で効率的な探索モジュールを提案する。 実験により,これらの軽量モジュールは小言語モデルの性能を効果的に向上することが示された。
  論文  参考訳（メタデータ） (2025-09-09T05:26:29Z)
• DLBacktrace: A Model Agnostic Explainability for any Deep Learning Models [1.747623282473278]
  深層学習モデル決定に対する明確な洞察を提供するために設計された,モデルに依存しない手法であるDLBacktraceを紹介する。 本稿では,DLBacktraceの概要を概説し,その性能を既存の解釈可能性手法と比較する。 その結果,DLBacktraceは多種多様なタスクにおけるモデル行動の理解を効果的に促進することを示した。
  論文  参考訳（メタデータ） (2024-11-19T16:54:30Z)
• Data-efficient Large Vision Models through Sequential Autoregression [58.26179273091461]
  限られたデータセットに基づいて,効率的な自己回帰に基づく視覚モデルを構築する。 このモデルは,高レベル・低レベルのセマンティック理解の両方にまたがる視覚的タスクにおいて,その習熟度をいかに達成するかを実証する。 我々の経験的評価は、モデルが様々なタスクに適応する際の機敏さを強調し、パラメータフットプリントの大幅な削減を図った。
  論文  参考訳（メタデータ） (2024-02-07T13:41:53Z)
• Do LVLMs Understand Charts? Analyzing and Correcting Factual Errors in Chart Captioning [90.13978453378768]
  生成したチャートキャプションに事実誤りを包括的に分類する。 大規模な人間のアノテーションの取り組みは、様々なチャートキャプションモデルによって作られたキャプションのエラーパターンと頻度に関する洞察を提供する。 分析の結果,GPT-4Vを含む最先端モデルでさえ,事実不正確なキャプションを頻繁に生成していることが判明した。
  論文  参考訳（メタデータ） (2023-12-15T19:16:21Z)
• Identifying and Mitigating Model Failures through Few-shot CLIP-aided Diffusion Generation [65.268245109828]
  本稿では,突発的相関に付随する障害モードのテキスト記述を生成するためのエンドツーエンドフレームワークを提案する。 これらの記述は拡散モデルのような生成モデルを用いて合成データを生成するのに使うことができる。 本実験では, ハードサブポピュレーションの精度(sim textbf21%$)が著しく向上した。
  論文  参考訳（メタデータ） (2023-12-09T04:43:49Z)
• Improving Input-label Mapping with Demonstration Replay for In-context Learning [67.57288926736923]
  In-context Learning (ICL)は、大規模な自己回帰言語モデルの出現する能力である。 Sliding Causal Attention (RdSca) と呼ばれる新しいICL法を提案する。 ICL実験において,本手法は入力ラベルマッピングを大幅に改善することを示す。
  論文  参考訳（メタデータ） (2023-10-30T14:29:41Z)
• LLM2Loss: Leveraging Language Models for Explainable Model Diagnostics [5.33024001730262]
  我々は、失敗とバイアスのモデルパターンに関するセマンティックな洞察を提供するアプローチを提案する。 このような軽量モデルのアンサンブルを用いて,ブラックボックスモデルの性能に関する洞察を得られることを示す。
  論文  参考訳（メタデータ） (2023-05-04T23:54:37Z)
• Large Language Models with Controllable Working Memory [64.71038763708161]
  大規模言語モデル(LLM)は、自然言語処理(NLP)の一連のブレークスルーをもたらした。 これらのモデルをさらに切り離すのは、事前訓練中に内在する膨大な量の世界的知識だ。 モデルの世界知識が、文脈で提示された事実情報とどのように相互作用するかは、まだ解明されていない。
  論文  参考訳（メタデータ） (2022-11-09T18:58:29Z)

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

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