ProGS 用基于模型的证明草图组织形式化建模，在 27 个形式系统基准上提升语法有效性、演绎可验证性与行为正确性
核心概要
该工作提出 Proof-Sketch-Guided Formal Model Synthesis（ProGS），一种以基于模型的证明草图为中心的自动形式化方法：草图把目标形式系统的证明结构表示为树，内部节点对应情况划分与归纳推理步骤，叶节点对应实现各子目标的具体状态转移事件，LLM 负责生成与修复这些草图，验证失败被映射回特定节点与子树以提供结构化修复指导；在 27 个形式系统基准上的评估显示，ProGS 在语法有效性、演绎可验证性与行为正确性上优于当前最先进的智能体式形式化建模方法。
Figure 2. Model-based proof sketches generated by ProGS . Green nodes denote termination cases, while blue nodes denote general cases introduced by case splitting. Each leaf node is annotated with its corresponding action. Each node is labeled with guards, where the common guards shared with its parent are omitted for simplicity.
arXiv深度剖析
ProGS 把形式模型构建组织为对“基于模型的证明草图”的生成与修复，草图以树结构表示目标形式系统的证明结构，内部节点承载情况划分与归纳推理步骤，叶节点对应实现各子目标的具体状态转移事件。 相对于以生成模型本身并用形式工具反馈修复的既有范式，这里把证明结构而非模型文本作为迭代的中心对象，使修复有明确的层级位置。 论文摘要给出方法定义与结构描述，属于概念与设计层面的说明。
ProGS 将验证失败映射回草图中的特定节点与子树，从而为迭代修复提供结构化指导。 既有生成—修复范式的修复由生成模型的验证失败驱动，依赖反馈粒度与 LLM 修复能力，且针对某一验证层级的修复可能使另一层级的性质失效，需要通盘推理全部事件守卫；把失败定位到草图节点改变了修复的作用范围。 摘要陈述了该机制及其针对的问题，未给出映射算法细节或消融数据。
在 27 个形式系统构成的基准上，ProGS 在语法有效性、演绎可验证性与行为正确性三项指标上优于当前最先进的智能体式形式化建模方法。 把改进同时落在三个不同层级的评价维度上，而不仅是单一验证通过率。 摘要报告了基准规模与相对比较结论，未在摘要中给出具体数值、逐项得分或统计检验。
启示与展望
该结果面向需要形式建模与演绎验证的系统，适用于以证明结构可被组织为树、且验证失败可定位到节点或子树为前提的建模任务；对希望减少形式建模人力与专长门槛的研究者与工程实践者，它提供了一条以草图为中心、由 LLM 生成与修复、并以结构化反馈迭代的路径。
摘要未给出三项指标的具体数值、逐系统结果、消融实验或统计检验，也未说明草图生成与修复的提示设计、失败映射的判定规则以及基准中形式系统的来源与难度分布；此外，摘要未讨论该方法在更大规模或不同形式工具链上的表现，这些是读者在采纳结论前仍会关注的问题。