用检索与智能体系统提升形式化证明生成效率
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
- 基于自注意力嵌入模型的检索机制选前提
- 生成性能最高提升28%，复杂定理成功率翻倍
- 多智能体辩论+反思机制适合高难度形式验证
交互式定理证明在结合生成式人工智能后展现出显著成效。本文评估了多种Rocq生成方法，揭示了基于检索的前提选择是高效生成的关键。提出一种基于自注意力嵌入模型的新方法，实验显示生成器性能最高提升28%。针对Rocq证明生成问题，设计了一种面向形式化验证的多阶段智能体系统，效果显著。消融实验证明，在规划阶段引入多智能体辩论，整体证明成功率提升20%，复杂定理成功率几乎翻倍；反思机制进一步增强了结果的稳定性和一致性。
原文摘要 · Abstract (English)
Interactive Theorem Proving was repeatedly shown to be fruitful when combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation and illuminates potential avenues for improvement. We identify retrieval-based premise selection as a central component of effective Rocq proof generation and propose a novel approach based on a self-attentive embedder model. The evaluation of the designed approach shows up to 28% relative increase of the generator's performance. We tackle the problem of writing Rocq proofs using a multi-stage agentic system, tailored for formal verification, and demonstrate its high effectiveness. We conduct an ablation study and demonstrate that incorporating multi-agent debate during the planning stage increases the proof success rate by 20% overall and nearly doubles it for complex theorems, while the reflection mechanism further enhances stability and consistency.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。