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.

翻译：交互式定理证明与生成式人工智能的结合已被多次证明成效显著。本文评估了多种Rocq生成方法，并揭示了潜在的改进方向。我们指出基于检索的前提选择是高效生成Rocq证明的核心环节，并提出一种基于自注意力嵌入模型的新方法。对所设计方法的评估表明，生成器的性能相对提升了最高达28%。我们采用专为形式化验证设计的智能体系统来解决Rocq证明书写问题，并验证了其高效性。通过消融实验，我们证明在规划阶段引入多智能体辩论机制能使整体证明成功率提升20%，对复杂定理的证明成功率提升近一倍，而反思机制则进一步增强了系统的稳定性与一致性。