FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization

先给结论

FormalEvolve 的贡献可以浓缩成一句话：在 Lean autoformalization 中，statement 本身是 prover-facing interface，不只是语义翻译终点；所以与其赌一个输出，不如在固定 generator-call 预算内构造一个去重的、语义通过的候选集合。

研究动机：为什么 single-output 不够

Autoformalization 表面上是把自然语言数学题翻译成 Lean statement。但本文强调，这个任务天然是 many-to-many：同一个 informal theorem 可以对应多个 faithful formal statements。问题在于，下游 proving 并不是只关心语义是否一致，还关心这个 formal statement 是否容易被 prover 搜索到证明。

换句话说，formal statement 有两层角色：第一，它是语义翻译结果；第二，它是 prover 看到的接口。即使两个 statement 都满足 \(\operatorname{CompOK}(c)=1\) 和 \(\operatorname{SemOK}(c)=1\)，它们在同一个 prover、同一个 attempt budget 下也可能产生完全不同的 proof outcome。

数学表示及建模

核心对象

给定 informal statement \(x\)，系统搜索 Lean 4 candidate \(c=(\hat{h}, y)\)。其中 \(\hat{h}\) 是 import/header context，\(y\) 是主要 Lean statement 或 declaration target。每个 candidate 要过两个门：

\(\operatorname{CompOK}\) 是 Lean 编译/ elaboration 门；\(\operatorname{SemOK}\) 是 CriticLean-Qwen3-14B 判断 statement 是否 faithfully formalizes \(x\)。archive 只允许 \(\operatorname{CompOK}(c)=1\) 的候选进入，但 archive 内可以保留 \(\operatorname{SemOK}(c)=0\) 的 stepping stones，因为它们可能提供有用的 binder、import 或结构。

真正报告的对象：semantically consistent repertoire

最终用于 SH@T 和 downstream proving 的不是 archive 全体，而是预算内生成的、去重后的语义通过集合：

这点很关键：archive 是搜索记忆，\(G_T\) 是评估与 prover 输入。论文避免了把“编译可行但语义错误”的 archive stepping stone 直接算作成功。

parent selection：质量与反复使用惩罚

在 island archive \(\mathcal{A}_I\) 中，候选 \(c_i\) 被选为 parent 的概率是：

权重由 gate score、robust normalization 和 usage penalty 组成：

因为 archive 里都已经 compile-ok，所以 \(\operatorname{SemOK}=0\) 的候选 \(s_i=1\)，\(\operatorname{SemOK}=1\) 的候选 \(s_i=2\)。\(u_i\) 则惩罚一个 parent 被反复抽中，降低 mode collapse。

concentration metric：不是只看覆盖率

论文特别避免“成功都集中在简单题”的假象。设 \(s_j(T)\) 是第 \(j\) 个 problem 在预算 \(T\) 内获得的 semantic-success candidate 数量，Gini 定义为：

低 Gini 和低 Top-10% share 表示 semantic successes 没有过度堆在少数 easy problems 上。

算法流程：compile-gated archive search

精简伪代码

Input: informal theorem x, budget T, seed model, patch model
Archive A = compile-feasible candidates
Accepted G = compile-ok and semantic-ok candidates

Seed A with initial candidates; debit calls
while budget remains and A is non-empty:
  sample island I
  sample parent p from A_I using weighted + usage-penalized rule
  sample archive context / inspiration candidates
  propose c via full / diff / cross patch
  if duplicate or compile fail:
      try EvolAST fallback; optionally bounded compile repair
  if compiles:
      judge semantic consistency
      insert compile-ok candidate into archive
      if semantic-ok: add to accepted repertoire G
      else optionally run bounded semantic repair
return Dedup(G)

实验方法与实验设计

实验设计的主线是：在固定 generator-call budget \(T=100\) 下比较 archive search 与 no-archive controls，再用固定 prover budget \(B=64\) 测试这些 statement repertoires 是否真的能转化成 proof utility。

为什么 matched Hybrid control 很重要

如果只和 Kimina baseline 比，FormalEvolve 的收益可能来自更强的 Qwen3 repair model。Hybrid control 把 seeding/repair stack 尽量对齐，但去掉 archive search，因此它是判断“archive 是否真的有用”的关键对照。

Prompt / repair 复现要点

初始生成和 evolution prompt 都要求输出完整 Lean 4 file，必须从 import Mathlib 和 import Aesop 开始，且包含 exactly one theorem，结尾是 := by sorry。compile repair 只修编译，不应改变语义；semantic repair 可以改 hypotheses/conclusion，但必须对齐原 informal statement，不能弱化成 tautology。

实验结果及核心结论

1. Statement generation：FormalEvolve 提高 semantic hit，也降低集中度

最清晰的结论是：相对 matched hybrid，FormalEvolve 在两个 benchmark 上都有 SH@100 增益，并且 Gini 更低。也就是说，它不只是多命中几个题，还让 semantic successes 更不集中。

2. Patch repair 是最直接的驱动，island/EvolAST 是更细的实现敏感项

移除 patch repair 后，CombiBench SH@100 从 0.580 掉到 0.470，ProofNet 从 0.849 掉到 0.780，说明 bounded repair 是最强的直接贡献。相比之下，\(K=1\)、\(K=2\)、w/o EvolAST 的差异更 dataset-dependent：它们说明实现细节重要，但不应该被过度解读成某个 island 设置绝对更优。

3. Downstream proof utility：repertoire 确实能帮 prover，但不是全面碾压

相对 Hybrid control，FormalEvolve 的 theorem-complete@64 在 CombiBench 从 9/100 到 13/100，在 ProofNet 从 40/186 到 45/186。但在 ProofNet 上，Kimina Compile+Semantic Repair 的 theorem-complete 是 46/186，略高于 FormalEvolve。这是一个重要边界：repertoire search 有帮助，但具体 prover utility 不是单调支配所有 baseline。

4. Manual audit：语义风险没有消失，只是被显式报告了

论文承认 \(\operatorname{SemOK}\) 来自 LLM-as-judge，所以做了人工 faithfulness audit。statement-stage matched ProofNet slice 中，FormalEvolve / Hybrid / Sample 的 Faithful/Partial/Severe 分别是 42/5/3、43/4/3、43/3/4。这个结果说明 archive search 没有明显放大 judge-positive semantic shift，但也说明 judge-positive 不是绝对可靠。

我的评论：优势、不足与改进方向

我会追问的 reviewer 问题

可能的改进方向

• 加入更强的 diversity metric：不仅按 problem-level success 分布，也按 Lean AST / theorem shape / binder structure 聚类。
• 对 prover utility 做 cross-prover 测试：同一 repertoire 在 Goedel、Kimina、不同 prompt policy 下是否仍有增益。
• 把 archive policy 学习化：parent selection 目前比较手工，未来可以把 judge/prover feedback 合成 bandit-style policy。
• 把 semantic judge 从单模型判定改成 calibration ensemble 或 verifier-augmented judge，降低 judge-positive 的系统性偏差。

One More Thing：这篇对“研究路线”的启发

我觉得这篇最值得带走的不是某个具体数字，而是一个范式：当一个任务的正确输出不是唯一的，且下游系统对输出形式敏感时，单输出评价会天然低估 test-time search 的价值。

这对 autoformalization 很明显，对代码生成、工具调用计划、证明策略生成也类似。一个 candidate 是否“语义正确”只是第一层；但“它是否能成为下游搜索系统的好接口”需要靠 proof utility 表和 prover outcome 读出，不能只从 semantic trace 图推出。

Reference / Evidence

公开版只列可公开访问的在线来源；私有源文件、内部目录和非公开运行记录不作为网页证据暴露。