FormalEvolve

审稿结论：Weak Accept，置信度 3/5。

贡献与新颖性：把 autoformalization 从单一 reference statement 的预测任务重写成固定预算下的 repertoire search，并将 compilation-feasible archive 与 semantic accepted repertoire 分离。这个 framing 与实验协议是一致的，不只是换了一个算法名称。

证据：matched Hybrid 使用相同 Kimina generation/Qwen3 repair stack 但移除 archive、parent reuse、archive context、usage penalty 与 migration；FormalEvolve 在 CombiBench 的 SH@100 为 0.580 vs 0.530，在 ProofNet 为 0.849 vs 0.828；theorem-complete@64 为 13/100 vs 9/100、45/186 vs 40/186。

主要保留：最大直接驱动力是 bounded patch repair；K=1 和 no-EvolAST 在部分指标上更强；semantic labels 依赖单一 CriticLean judge，proof utility 依赖单一 Goedel prover/B=64。论文支持“在此协议下的 archive search 增益”，不支持跨 judge/prover 的普遍定律。

时间线定位：FormalEvolve 的 arXiv v1 提交日期为 2026-03-20，当前 arXiv 页面显示在线版本日期为 2026-05-28；作者为 Haijian Lu、Wei Wang、Jing Liu。它位于 Lean autoformalization、formal theorem proving 与 evolutionary search 的交叉处。

关键前作 1 — ProofNet：Azerbayev et al. 的 ProofNet 把本科数学自然语言题、Lean formal statement 和 proof 组织成 benchmark。FormalEvolve 直接使用 ProofNet Lean 4 test split（N=186），继承了“自然语言到可编译形式化再到证明”的评测链，但把单个参考 statement 改成多个语义接受候选的 repertoire。ProofNet 因而是它的问题坐标系，而不是普通 related-work 背景。

关键前作 2 — EvolProver：Tian et al. 的 EvolProver 研究通过对形式化问题做保持语义/结构的 symmetry 变换来扩充和演化 prover-facing 数据。FormalEvolve 明确将其作为 EvolAST fallback 的灵感来源：只改 binder type 与 goal type，保持 imports/preamble 不变，并把生成候选重新送入同一编译门和 semantic judge。这是具体机制继承，不是泛泛引用。

已验证的两个后续引用：Google Scholar 对 arXiv:2603.19828 的结果显示 Cited by 2（检索日期 2026-08-08）：

1. What are the Right Symmetries for Formal Theorem Proving?（Olejniczak et al., arXiv:2605.22257）。它研究语义等价但 prover effectiveness 不同的表示，并把 FormalEvolve 放进“representation/symmetry affects formal proving”的后续脉络。
2. Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning（Feng & Shi, arXiv:2606.15972）。其题目和摘要聚焦 Lean-based answer selection；Google Scholar 将其列为引用 FormalEvolve 的后续工作，说明 repertoire/statement selection 的问题正在向答案选择与证明效率方向扩展。

考古结论：FormalEvolve 不是凭空出现的“LLM+进化”，而是把 ProofNet 的 benchmark、EvolProver 的结构变换和 prover-sensitive representation 线索合成为 test-time archive search；随后两篇工作又把“表示选择影响证明”推进到更显式的 symmetry 分析和 answer selection。

后续项目：Prover-Portfolio Allocation from Accepted Repertoires。

这不是从 workspace 中其他项目移植来的设计，而只使用本文已公开的事实：FormalEvolve 产生多个去重、compile-ok、semantic-judge-positive 的候选，并在 B=64 下观察到候选之间 proof outcome 不同。

新项目把 prover 从固定评测器变成预算分配对象。先用少量 probe attempts 估计每个 statement 的 prover compatibility，再在总 token/FLOPs/attempts 固定的情况下，把剩余预算分给互补 statements 或不同 prover。对照包括 uniform allocation、只看 semantic score 的 selector、只看 prover probe 的 selector 和联合 selector。

只有 FormalEvolve 成功后才可能：没有它提供的同题多候选 repertoire，就没有 candidate × prover routing 的对象；单一 top-1 autoformalizer 只能研究“生成得对不对”，不能研究“哪个忠实接口值得给哪个证明器多少预算”。

成功标准：跨两个 judge、两个 prover 和 matched total compute，联合 selector 提升 theorem-complete@B，并且不通过牺牲 faithfulness 换取证明率。

产品提案：数学教材的形式化接口候选生成器。出版社或教育平台上传一道自然语言定理，系统输出多份可编译、语义评分过关的 Lean statements，再交给固定 prover 排序，减少形式化工程师从空白文件到可审校候选的成本。

正面影响：扩大形式化教材覆盖、展示同一命题的多种编码，并保留失败轨迹供教师审查。

负面影响：judge-positive 的语义漂移可能被 UI 误包装成“已验证”，且 T=100/B=64 的调用成本和能耗不低。部署必须分层显示 compile、semantic audit、proof complete 三种状态，并要求人类签核。

这是一个真正的机制 demo，而不只是伪代码：动画把整条 pipeline 展开，显示 informal theorem 如何经过 seedbank、编译门、archive、patch/repair、semantic judge、EvolAST、repertoire，最后进入固定 B=64 prover。

可运行 toy 核心：在 3 个小型 Lean statement 上，archive 只保存 `lake env lean` 编译成功的 canonical candidates；mutation 用手写 binder/等式改写，semantic gate 用公开的 toy truth table。它的核心路径是按论文伪代码独立写的，不是下载现成实现；动画是解释器，不冒充论文实验复现。

while calls < T and archive:
    parent = weighted_sample(archive, usage_penalty=True)
    candidate = mutate(parent)
    calls += 1
    if lean_compiles(candidate):
        archive.add(canonicalize(candidate))
        if toy_semantic_gate(candidate):
            repertoire.add(candidate)
return dedup(repertoire)

调查边界：只使用公开学术资料，不联系作者，不推断私人信息。

作者与机构：论文 TeX 的作者块明确写出：Haijian Lu^1,2、Wei Wang²、Jing Liu¹；¹ 为 School of Artificial Intelligence, Xidian University, Xi’an；² 为 Beijing Institute for General Artificial Intelligence (BIGAI), Beijing。作者顺序与 arXiv 页面一致。

通讯作者：Wei Wang 在 TeX 中带有 `Corresponding author: wangwei@nlpr.ia.ac.cn`。这里可以确认通讯邮箱域名为 NLPR/IA 体系，但不能仅凭邮箱把其当前机构扩张成论文未写出的其他任职事实。

公开研究轨迹：Google Scholar 的 H Lu profile 将 Haijian Lu 列为作者；同一 profile 的论文列表与 FormalEvolve 的 autoformalization/formal reasoning 方向相符。需要特别注意：Google Scholar 的“Wang Wei”候选页显示的是另一位视觉/动作识别研究者，无法安全确认就是本文通讯作者，因此新版不把它写入作者履历。对 Jing Liu，本次没有找到足以完成同名消歧的可靠公开 profile，也不编造履历。

研究动机链：从论文公开轨迹可确认的共同主题是 Lean/formal mathematics、LLM-based theorem proving、statement representation 与 evolutionary search；这些内容直接解释了为什么三位作者会合作研究 FormalEvolve。至于个人职业经历、教育经历和未公开动机，当前证据不足，不应写成事实。

结论：这次能确认作者机构、通讯作者和研究主题，但对 Wei Wang/Jing Liu 的个人主页级履历仍需更强的同名消歧证据；“不知道”比错认同名作者更可靠。

论文自评：论文把影响主要表述为技术效用：多样化、semantic-accepted statements 在固定 prover budget 下提高找到 prover-friendly formulation 的概率；limitations 同时承认 compilation/proof 不等于对自然语言原题的忠实。

额外正面影响：repertoire 能帮助教学、benchmark 诊断、人工审校和形式化接口设计，而不是只追求 top-1。

遗漏的负面影响：单一 judge 的偏差可能被 archive 反复放大；T=100/B=64 提高算力门槛；高风险验证场景可能出现“形式上证明了错误对象”；archive 可能积累 benchmark-specific shortcuts。部署应公开成本、失败案例与 judge agreement，并保留人工语义门禁。