FormalEvolve：神经符号进化搜索多样化且经证明有效的自动形式化

自动形式化旨在将自然语言数学转化为可编译、机器可检查的语句。然而，语义一致性并不意味着证明者的有效性：即使语义一致的形式化在证明搜索成本和成功率方面也可能存在很大差异。在这项工作中，我们将自动形式化表述为一种预算内的、测试时搜索语义一致的指令集，并提出了 FormalEvolve，一种编译门控神经符号进化框架。 FormalEvolve 通过 LLM 驱动的突变和有界补丁修复的交叉生成不同的候选者，而符号抽象语法树 (AST) 重写操作进一步注入结构多样性。在 CombiBench 和 ProofNet 上，在 T = 100 的严格生成器调用预算下，FormalEvolve 达到了 58.0% 和 84.9% 的语义命中率 (SH@100)，并降低了语义成功的跨问题集中度（较低的基尼系数）。在固定的验证预算下，FormalEvolve 还提高了 CombiBench 上的下游验证性能。代码将公开发布。