发表机构
City University of Hong Kong; Northeastern University (China); Northeast Forestry University; University of Electronic Science and Technology of China; Southeast University; Uppsala University（香港城市大学; 东北大学（中国）; 东北林业大学; 电子科技大学; 东南大学; 乌普萨拉大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
ProsaBuddy利用LLM智能体系统，通过ReAct循环和子目标委派架构，降低在Rocq中构建机械化实时调度性证明的难度，并在基准上显著优于现有方法。
AI 中文摘要
严格的调度性分析对于硬实时系统的设计至关重要，然而纸笔证明中的错误威胁着关键应用的安全性。Prosa倡议通过为在Rocq证明助手中构建机器可检查的调度性分析证明提供基础来解决这一问题。然而，构建此类证明所需的大量时间和专业知识仍然是Prosa更广泛采用的主要障碍。本工作提出了ProsaBuddy，一个基于LLM的智能体系统，旨在降低开发机械化实时调度性证明所需的努力。ProsaBuddy采用带有检索的ReAct循环，检索Prosa代码库，访问Rocq工具以及可选的人工提示。它使用子目标委派架构，将引理分解为子目标，并将它们分派给子智能体进行证明。我们在从实时调度文献中提取的迷你基准上评估了ProsaBuddy。实验结果表明，ProsaBuddy显著优于最先进的基于LLM的Rocq自动证明智能体系统和通用编码智能体OpenCode。
英文摘要
Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa. This work presents ProsaBuddy, an LLM?based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints. It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof. We evaluate ProsaBuddy on a mini benchmark drawn from real-time scheduling literature. Experiment results show that ProsaBuddy significantly outper?forms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode
CommentsAccepted at RTSS 2026
