arXiv cs.AI· Peter Dolog, Kim G. Larsen, Marius Miku\v{c}ionis, Frederik F. K. Rasmussen·· 13 小时前AI 评分31
UPPAAi：面向 LLM 辅助建模、验证、分析与综合的 UPPAAL 扩展
UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis
AI 导读
UPPAAi 是 UPPAAL 的扩展，让用户通过与 LLM 对话来构建、解释、调试和规约模型，遵循"用户请求、LLM 提议解释与编排、UPPAAL 验证"的原则。它通过 Tools API 开放 UPPAAL 编辑器、查询与验证器，并报告了 7 个案例研究，覆盖时间自动机、随机混合自动机和策略学习。研究显示 LLM 不仅能生成方案，还会主动建议用户未询问的相关 UPPAAL 功能。
正文 · AI 翻译
摘要：三十多年来，UPPAAL 一直支持实时系统和信息物理系统的建模与分析。然而，构建合适的模型、形式化预期性质、选择分析技术以及解释反例仍然是需要大量专业知识的迭代任务。大语言模型（LLM）可以提供看似合理的解释甚至解决方案，但它们不一定正确。我们提出 UPPAAI，这是 UPPAAL 的一个扩展，用户可以在与 LLM 的对话中构建、解释、调试和规约模型。其指导原则是：用户提出请求，LLM 提出建议、解释并编排，UPPAAL 进行验证。UPPAAI 通过 Tools API 开放 UPPAAL 编辑器、查询和验证器。我们报告了七个案例研究，从向新手解释到学习控制器，涵盖时间自动机、随机混合自动机和策略学习。LLM 被证明极其有用，不仅在于生成解决方案，还在于主动建议未被问及的相关 UPPAAL 功能。
| 评论： | 提交至 IFS/ETAPS 2027 |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2610.40042 [cs.SE] |
| （或 arXiv:2610.40042v1 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.40042 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Marius Mikučionis [查看电子邮件]
[v1]
2026年10月29日星期四 13:40:33 UTC（746 KB）
来源：arXiv cs.AI · arxiv.org