自动优化方法能提升形式化验证中的证明代理性能。
RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
- 用自动优化器改进Rocq系统中的证明生成代理。
- 少量示例引导效果最好，但仍不及人工精心设计的顶尖代理。
- 适合对AI代理自动化调优感兴趣的验证研究者。
本研究探讨自动AI代理优化方法在真实世界形式化验证场景中的适用性，以Rocq系统中的自动化定理证明为典型且具挑战性的领域。我们评估不同自动代理优化器在优化Rocq证明生成代理任务中的表现，并检验代理系统中精细调优部分（如提示设计、上下文知识、控制策略）是否可自动化。结果表明，尽管多种优化器带来可测量的性能提升，但简单的少样本引导最为稳定有效；然而，所研究的方法均未达到精心设计的前沿证明代理水平。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。