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

全证明自动形式化旨在将自然语言数学证明转化为形式化验证推理。针对现有方法训练成本高或推理修复盲目等问题，本文提出 ToMap 多智能体框架。该框架将任务分解为分解器、形式化器和证明器流水线，并通过瓶颈分析发现分解器是关键。ToMap 聚焦于分解器的测试时优化，利用形式化验证进度和语义评分构建帕累托前沿，引导提示词进化。实验表明，该方法在语法正确性和语义忠实度上显著优于前人工作，且计算成本更低。