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

自动形式化旨在将自然语言数学转化为可编译、机器可验证的陈述。然而，语义一致性并不等同于证明器有效性。本文将其表述为预算约束下的测试时搜索问题，并提出 FormalEvolve，一种编译门控的神经符号进化框架。该方法通过 LLM 驱动的突变与交叉生成多样候选，结合符号抽象语法树重写注入结构多样性。实验表明，在严格调用预算下，该方法显著提升了语义命中率并降低了成功分布集中度，同时改善了下游证明性能。