[Paper] ModelWisdom：一个用于 TLA+ 模型可视化、摘要与修复的综合工具包

Source: arXiv - 2602.12058v1

请提供您希望翻译的具体文本内容，我将按照要求保留源链接并将文本翻译成简体中文。

概述

使用 TLA+ 进行模型检查可以证明系统是正确的，但当属性失效时，原始的反例输出往往难以阅读。作者们推出了 ModelWisdom，这是一套集成工具包，将交互式可视化与大语言模型（LLM）辅助相结合，使得 TLA+ 调试更加快速、清晰且更易于工程师上手。

关键贡献

• 交互式模型可视化 – 颜色编码的违规高亮、可点击的边缘跳转至原始 TLA+ 代码，以及违规状态与破坏的时序属性之间的显式链接。
• 图形优化与折叠 – 基于树的布局，自动节点/边缘折叠，使大型状态转移图保持可导航。
• 模型摘要 – 由 LLM 驱动的子图摘要，提供自然语言解释，说明一簇状态代表的含义。
• 模型修复助手 – 自动提取错误信息并建议纠正措施，实现“调试‑建议‑应用”的迭代循环。
• 开源原型 – 公共托管的网页界面 (https://model-wisdom.pages.dev) 和演示视频，鼓励社区采用和进一步研究。

方法论

1. 数据管道 – 工具包使用标准的 TLC 模型检查器跟踪文件（状态、操作和被违反的不变式）。
2. 图构建 – 预处理步骤构建有向图，然后应用基于树的重构算法，将相似的执行路径分组并识别可折叠的子结构。
3. 可视化层 – 使用现代的基于网页的图形库，系统渲染优化后的图，并使用自定义样式（例如，违规转移用红色，满足的用绿色）。UI 钩子将每个可视元素映射回原始的 TLA+ 源代码行。
4. LLM 集成 – 选定的子图会被送入提示流水线（例如 GPT‑4），让模型“解释这簇状态的作用”以及“为突出显示的违规提供修复建议”。生成的文本会与图一起显示。
5. 修复循环 – 当开发者接受建议的修复时，ModelWisdom 可以自动编辑 TLA+ 规范（或生成补丁）并重新运行 TLC，闭合反馈循环。

结果与发现

• 可用性研究 – 在一次小规模用户研究（8 位参与者，对 TLA+ 经验混合）中，定位违规根本原因的平均时间从 23 分钟（基线 Toolbox）降至使用 ModelWisdom 的 7 分钟。
• 可扩展性 – 对拥有 > 10 k 状态的模型，图折叠将视觉杂乱度降低了最高 85 %，并在普通笔记本电脑上保持帧率高于 30 fps。
• LLM 摘要 – 参与者在 71 % 的情况下将自动生成的摘要评为“有帮助”或“非常有帮助”，表明自然语言解释可以有意义地补充形式化产物。
• 修复成功率 – 修复助手对 7 个有意植入的错误中 6 个提供了正确的修复建议，证明提取的错误上下文足以支持可操作的推荐。

实际意义

• 更快的调试周期 – 工程师可以在不手动筛选大量 TLC 日志的情况下定位并修复规范错误，加速安全关键系统（例如分布式协议、硬件控制器）的开发。
• 降低入门门槛 – 可视化和叙事辅助使得对代码熟悉但不熟悉形式化方法的开发者更容易上手 TLA+，有望在业界扩大其采纳。
• 集成潜力 – ModelWisdom 的模块化流水线可以接入 CI/CD 流程：TLC 运行失败时可自动生成可视化报告和建议补丁，将模型检查提升为一等质量门槛。
• 跨工具协同 – 折叠和 LLM 驱动的摘要概念可以移植到其他模型检查生态系统（如 SPIN、Alloy），提供可复用的可解释验证模式。

限制与未来工作

• LLM 依赖 – 摘要和修复建议的质量取决于底层语言模型；噪声或模糊的输出可能误导用户。
• 可扩展性上限 – 虽然折叠有帮助，但极大的模型（> 100 k 状态）仍会给浏览器渲染和 LLM 提示长度限制带来压力。
• 用户研究规模 – 本次评估的参与者数量有限；需要更大范围的工业试验来验证实际影响。
• 未来方向 – 作者计划 (1) 集成经过微调的领域特定 LLM，以提供更准确的解释；(2) 添加团队协作调试功能；(3) 探索自动抽象技术，进一步压缩庞大的状态图。

作者

• Zhiyong Chen
• Jialun Cao
• Chang Xu
• Shing‑Chi Cheung

论文信息

• arXiv ID: 2602.12058v1
• 分类: cs.SE, cs.AI, cs.FL
• 发表时间: 2026年2月12日
• PDF: 下载 PDF