ProsaBuddy 用 LLM 智能体自动证明实时可调度性引理，在小型基准上显著优于现有 Rocq 证明智能体与通用编码智能体 OpenCode

ProsaBuddy 是一个面向机械化实时可调度性证明的 LLM 智能体系统，目标是降低在 Rocq 证明助手内基于 Prosa 构建机器可检验证明所需的投入。 既有 Prosa 提供机器可检验的可调度性分析证明基础，但构建此类证明需要大量时间与专业知识，构成推广障碍；该工作把 LLM 智能体引入这一证明构建环节。 证据来自摘要层面的系统描述与评测陈述，未提供具体证明数量、成功率数值或基准规模。

系统采用 ReAct 循环，结合对 Prosa 代码库的检索、对 Rocq 工具的访问以及可选的人工书写提示。 将检索、工具调用与人工提示作为可选输入整合进同一智能体循环，而非仅依赖模型自身生成证明脚本。 摘要明确列出这三项机制，但未给出检索粒度、工具接口细节或提示注入方式。

系统使用子目标委派架构，把一条引理分解为若干子目标并分派给子智能体分别证明。 以分解—分派的方式组织证明搜索，区别于单一智能体端到端证明。 摘要给出架构描述，未报告分解策略的消融实验或子目标粒度的影响。

在取自实时调度文献的小型基准上，ProsaBuddy 显著优于现有基于 LLM 的 Rocq 自动证明智能体系统以及通用编码智能体 OpenCode。 把比较对象同时覆盖专用 Rocq 证明智能体与通用编码智能体，给出相对两类基线的性能位置。 摘要仅以“显著优于”表述结果，未给出基准条目数、通过率或统计检验细节。

该结果面向在 Rocq 证明助手中基于 Prosa 构建机器可检验实时可调度性证明的场景，适用于希望降低证明构建投入的实时系统与形式化方法研究者。系统设计上支持可选的人工书写提示，说明其定位是辅助而非完全替代人工证明工作。评测范围是取自实时调度文献的小型基准，因此结论适用于该基准所覆盖的引理类型与证明任务。

本次读取范围仅为摘要，未包含正文、图表与实验细节，因此基准的具体条目数、成功率数值、与各基线的逐项对比以及统计显著性均无法在此确认。子目标委派架构在不同引理结构下的表现、检索与人工提示各自带来的增益，以及系统在更大规模证明任务上的行为，仍是值得关注的开放问题。