RocqStar：利用相似性驱动检索与智能体系统进行Rocq生成
机器学习
2026-01-27 v3 人工智能
计算机科学中的逻辑
软件工程
摘要
交互式定理证明在与生成式人工智能结合时已被反复证明卓有成效。本文评估了多种Rocq生成方法，并阐明了潜在的改进途径。我们将基于检索的前提选择确定为有效Rocq证明生成的核心组件，并提出了一种基于自注意力嵌入器模型的新方法。对所设计方法的评估表明，生成器的性能相对提升了高达28%。我们使用专为形式化验证定制的多阶段智能体系统来解决编写Rocq证明的问题，并展示了其高度的有效性。我们进行了消融研究，并证明在规划阶段引入多智能体辩论使证明成功率总体提高了20%，对于复杂定理几乎翻倍，而反思机制进一步增强了稳定性和一致性。
引用
@article{arxiv.2505.22846,
title = {RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation},
author = {Andrei Kozyrev and Nikita Khramov and Gleb Solovev and Anton Podkopaev},
journal= {arXiv preprint arXiv:2505.22846},
year = {2026}
}