ToMap：面向多智能体证明自动形式化的高效测试时优化

ToMap将完整证明自动形式化拆分为分解、形式化和证明三个多智能体环节，并通过瓶颈分析发现分解器最关键。方法借鉴GEPA，仅集中测试时计算优化原子化证明单元，以形式验证进展和语义评分驱动迭代，在ProofFlowBench上较此前最佳方法提升19.0%，同时降低测试时成本。