RocqSmith：自动优化能锻造更好的证明智能体吗？

本研究探讨自动AI智能体优化方法在形式化验证场景下真实智能体中的适用性，聚焦Rocq中的自动定理证明这一具有代表性且具挑战性的领域。我们评估了不同的自动智能体优化器在优化Rocq证明生成智能体这一任务上的表现，并评估智能体系统中的部分细粒度调优（如提示设计、上下文知识和控制策略）能否被自动化。我们的结果表明，尽管若干优化器带来了可衡量的改进，但简单的少样本引导（few-shot bootstrapping）最为持续有效；然而，所研究的方法均无法匹敌一个精心工程化的最先进证明智能体的性能。