PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

📄 arXiv: 2608.12762v1 📥 PDF

作者: Sadat Shahriyar, Shareef Ahmed, Abdullah Al Arafat

分类: cs.AI

发布日期: 2026-08-13

💡 一句话要点

提出PROVE-RT以解决实时系统的可调度性分析问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 实时系统 可调度性分析 机械化证明 大型语言模型 自动化验证 PROSA ROCQ 文档检索

📋 核心要点

  1. 现有的可调度性分析方法依赖于纸笔证明，难以扩展和维护，缺乏有效的自动化支持。
  2. PROVE-RT框架利用大型语言模型生成PROSA/ROCQ脚本，通过依赖感知草图和文档检索来提高生成效率。
  3. 实验结果显示，PROVE-RT在生成有效PROSA机械化方面的成功率为44.7%，显著高于直接提示LLMs的效果。

📝 摘要（中文）

可调度性分析对于认证实时系统至关重要，但现有测试通常依赖于难以扩展、验证和维护的纸笔证明。PROSA/ROCQ中的机械化验证提供了严格的替代方案，但手动构建这些证明需要大量的领域专业知识和证明工程工作。本文提出了PROVE-RT，一个利用大型语言模型（LLMs）生成PROSA/ROCQ脚本的框架，以机械化实时系统文献中的可调度性分析。PROVE-RT通过依赖感知的非正式草图、从处理过的PROSA文档中检索、分阶段生成骨架和完成证明来指导生成。在经过策划的评估集上，直接提示最先进的LLMs未能可靠生成有效的PROSA机械化，而PROVE-RT的成功率达到了44.7%。这些结果表明，检索引导和分阶段的LLM辅助可以改善PROSA/ROCQ中可调度性分析的自动机械化。

🔬 方法详解

问题定义：本文旨在解决实时系统可调度性分析中的机械化验证问题。现有方法依赖于手动构建的纸笔证明，难以扩展、验证和维护，且需要大量领域知识和工程努力。

核心思路：PROVE-RT框架的核心思想是利用大型语言模型（LLMs）生成PROSA/ROCQ脚本，通过依赖感知的非正式草图和文档检索来指导生成过程，从而降低人工干预的需求。

技术框架：该框架包括多个主要模块：依赖感知的非正式草图生成、从处理过的PROSA文档中检索信息、分阶段生成脚本骨架以及完成证明的步骤。这些模块协同工作，以实现高效的脚本生成。

关键创新：PROVE-RT的主要创新在于结合了依赖感知的生成方法与文档检索技术，显著提高了生成有效PROSA机械化的成功率。这一方法与传统的手动证明方法本质上不同，后者往往缺乏自动化支持。

关键设计：在设计中，PROVE-RT使用了特定的参数设置和损失函数，以优化生成过程。此外，网络结构方面，采用了适合处理非正式草图和文档检索的模型架构，以确保生成的脚本符合PROSA的要求。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在实验中，PROVE-RT在生成有效的PROSA机械化方面取得了44.7%的成功率，显著高于直接提示最先进LLMs的效果。这一结果表明，检索引导和分阶段的LLM辅助显著改善了可调度性分析的自动化过程。

🎯 应用场景

该研究的潜在应用领域包括实时系统的设计与验证，尤其是在航空航天、汽车和工业自动化等关键领域。通过提高可调度性分析的自动化水平，PROVE-RT能够降低开发成本，缩短验证周期，提升系统的可靠性与安全性。未来，该框架可能会扩展到其他形式的机械化证明和验证任务中。

📄 摘要（原文）

Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in PROSA/ROCQ offers a rigorous alternative, yet manually constructing such proofs requires substantial domain expertise and proof-engineering effort. Recent successes of large language models (LLMs) across a wide range of tasks make them promising candidates for generating PROSA/ROCQ scripts for mechanized theorem provers. However, state-of-the-art LLMs often lack the PROSA-specific knowledge required to correctly use its modeling abstractions and proof patterns. This paper introduces PROVE-RT, an LLM-assisted framework for generating PROSA/ROCQ scripts to mechanize schedulability analyses in real-time systems literature. PROVE-RT guides generation through dependency-aware informal sketches, retrieval from processed PROSA documentation, staged skeleton generation, and proof completion. We construct a mechanization-oriented corpus from 1, 191 real-time systems papers, containing 13, 134 informal sketches with dependency information. On a curated evaluation set, direct prompting of state-of-the-art LLMs fails to reliably generate valid PROSA mechanizations, whereas PROVE-RT achieves a success rate of 44.7%. These results show that retrieval-guided and staged LLM assistance can improve automated mechanization of schedulability analysis in PROSA/ROCQ.