Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean 事件

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean arXiv:2606.04883v1 Announce Type: new Abstract: Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this