RocqSmith: 自动优化能否打造更优的证明代理？
RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
AI总结：
RocqSmith研究自动优化方法在提升证明代理性能上的效果，发现简单引导方法效果最佳，但无法超越精心设计的证明代理。
摘要：
本文研究了自动AI代理优化方法在形式验证设置中应用于现实世界代理的适用性，重点在于Rocq中的自动定理证明作为代表性和具有挑战性的领域。我们评估了不同自动代理优化器在优化Rocq证明生成代理任务中的表现，并评估了是否可以自动化代理系统中的细粒度调优部分，如提示设计、上下文知识和控制策略。我们的结果表明，尽管几种优化器能带来可测量的提升，但简单的少样本引导是效果最一致的；然而，没有任何研究方法能匹配精心设计的最先进的证明代理的性能。
英文摘要：
This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq as a representative and challenging domain. We evaluate how different automatic agent optimizers perform when applied to the task of optimizing a Rocq proof-generation agent, and assess whether parts of the fine-grained tuning of agentic systems, such as prompt design, contextual knowledge, and control strategies, can be automated. Our results show that while several optimizers yield measurable improvements, simple few-shot bootstrapping is the most consistently effective; however, none of the studied methods matches the performance of a carefully engineered state-of-the-art proof agent.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
