编辑做了个实验：把同一道题发给 64
个学生，每人配一位不同的译员，每稿只出一种忠实译法。结果戏剧性分化——同一道题，有的译法下大半学生能解，有的译法下全军覆没。译文"对不对"和译文"有没有用"，是两件事：题面只要换个说法定理结构就变（比如把"for all x, f(x) > 0"写成"the infimum of f is positive"），证明器看到的可攻击面完全不同。
顺着走一步：接口基准（equivalence-class benchmark）。评分单位从"候选-参考匹配"改成"类供给"：① 每题报告类级 utility
曲线（best-1/best-k under prover budget，FE 的 RR64
协议已经是现成读数）；② 数据集汇总报告"类覆盖率"而非"题覆盖率"；③ 附带
budget-constrained representative selection——给定 prover
预算，从档案选 k
个代表，测的是"这套数据管线能喂出多强的下游"。基准从考卷变成数据供给合同，评测与训练在同一个对象上闭环。
注意边界：这是本页在论文证据上外推的研究提议，不是论文已验证的内容。FE
没有做 prover 训练实验（PU
是评估，不是训练收益）；"类级评分更公平"目前只有 PN 单点证据（45 vs
34）与 CB 反向证据（GT 18 vs 13）并存。
Other Discussion Roles / 其他讨论角色
以下七个角色使用 MIT MAS.S60 课程原始
prompt，从不同责任位置审视同一篇论文。
Scientific Peer Reviewer
The paper has not been published yet and is currently submitted to a
top conference where you’ve been assigned as a peer reviewer.
Complete a full review of the paper answering all prompts of the
official review form of the top venue in this research area (e.g.,
NeurIPS). This includes recommending whether to accept or reject the
paper.
This paper was found buried under ground in the desert. You’re an
archeologist who must determine where this paper sits in the context
of previous and subsequent work. Find and report on one older paper
cited within the current paper that substantially influenced the
current paper and one newer paper that cites this current paper.
You’re a researcher who is working on a new project in this area.
Propose an imaginary follow-up project not just based on the current
but only possible due to the existence and success of the current
paper.
项目：Prover-Transfer Atlas（证明器迁移图谱）——把"prover-facing
interface"从口号变成测量。只有 FE 成功之后这个项目才可能：它需要 FE
已经造出的两样东西——跨题多样候选档案的生产能力，和 matched
预算协议的评估纪律。做法：固定候选侧（同一批 FE 档案），在 3
个异构 prover（Goedel-Prover-V2、Kimina-Prover、LeanDojo/ReProver
系）下跑同一 B
预算，产出接口敏感度矩阵——同一候选在不同 prover
下的 utility 相关性。两个可证伪预测：①
若"prover-facing"为真，矩阵显著偏离单位阵（候选对 prover
有"口味"匹配）；② 若 FE 增益只是数据多样性，矩阵接近单位阵（哪个
prover 都一样受益）——假说被干净地杀死。再加一步跨 prover
迁移（档案在 A 上建、喂给 B）与一个 explore/exploit 策略学习器（用
seed-先验错位度预测该用 K=1 还是
K=2+EvolAST，直接把论文的消融不对称升级成方法）。这个项目同时补上本页评论第
4 条指出的最大未闭合环。
Industry Practitioner
You work at a company or organization developing an application or
product of your choice (that has not already been suggested in a
prior session). Bring a convincing pitch for why you should be paid
to implement the method in the paper, and discuss at least one
positive and negative impact of this application.
You’re a hacker who needs a demo of this paper ASAP. Implement a
small part or simplified version of the paper on a small dataset or
toy problem. Prepare to share the core code of the algorithm to the
class and demo your implementation. Do not simply download and run
an existing implementation – though you are welcome to use (and give
credit to) an existing implementation for “backbone” code.
import random, warnings
K, CAP, T, BETA, LAM = 2, 40, 100, 0.05, 10
PREDS = ["x%2==0", "x%3==0", "x%2==1", "x<10", "x>=10", "x>5", "x<=5"]
TRUTH = lambda x: x % 2 == 0 and x >= 10 # 隐藏真值（"judge oracle"）
SAMPLES = list(range(30))
def comp_ok(c): # “Lean 编译门”→ 语法+可执行门
try:
with warnings.catch_warnings(): # 变异垃圾会触发 SyntaxWarning，属预期
warnings.simplefilter("ignore")
f = eval("lambda x: " + c)
[f(x) for x in SAMPLES]
return f
except Exception:
return None
def sem_ok(f): # “语义 judge”→ 机器 oracle（toy 专属简化）
return all(f(x) == TRUTH(x) for x in SAMPLES)
def canon(c): # canonicalization 去重（whitespace/命名归一）
return " ".join(c.replace("(", " ( ").replace(")", " ) ").split())
def fresh(rng): # full 算子：从模板重新生成
toks = [rng.choice(PREDS)]
while len(toks) < 7 and rng.random() < 0.35:
toks += [rng.choice(["and", "or"]), rng.choice(PREDS)]
return " ".join(toks)
def diff_edit(parent, rng): # diff 算子：token 级最小改动
toks = parent.split()
i = rng.randrange(len(toks))
if rng.random() < 0.5:
toks[i] = rng.choice(PREDS + ["and", "or"]) # 换一个 token
else:
j = rng.randrange(1, len(toks) + 1) # 只在 token 边界后插入
toks[j:j] = [rng.choice(["and", "or"]), rng.choice(PREDS)] # 增一个合取项
return " ".join(toks)
def cross(parent, inspir, rng): # cross 算子：把灵感里的谓词嫁接进父代
a, b = parent.split(), inspir.split()
j = rng.randrange(1, len(a) + 1) # 只在 token 边界后嫁接
a[j:j] = [rng.choice(["and", "or"]), b[rng.randrange(len(b))]]
return " ".join(a)
def evolast(c, rng): # EvolAST 回退：结构性强制变异
toks = c.split()
j = rng.randrange(len(toks))
if toks[j] in ("and", "or"):
toks[j] = "or" if toks[j] == "and" else "and"
else:
toks[j] = "not (%s)" % toks[j]
return " ".join(toks)
def repair(c, rng): # 有界修复：最多 2 次
for _ in range(2):
f = comp_ok(c)
if f is not None:
return c, f
toks = c.split()
if len(toks) > 1: # 删一个 token 常能修好语法
del toks[rng.randrange(len(toks))]
c = " ".join(toks)
return c, comp_ok(c)
def parent_select(island, rng): # 使用惩罚的加权父选择
recs = [r for r in island]
if not recs:
return None
w = []
for r in recs:
s = 1 + r["sem"] # s = CompOK*(1+SemOK)，入档必编译
u = 1.0 / (1 + (1 + BETA) * r["n"]) # 使用折扣
w.append(u * (1.0 + LAM * (s - 1))) # 软加权（sigmoid 的线性替身）
return rng.choices(recs, weights=w)[0]
def run(evolve=True, seed=0):
rng = random.Random(seed)
isl = [[] for _ in range(K)] # K 个半隔离岛，全局容量 CAP
seen, hits = set(), set()
for t in range(T): # T=100 generator calls，逐调用记账
parent = None
if evolve and any(len(I) for I in isl):
k = rng.randrange(K) # 采样一个岛，父代/灵感限于岛内
home = isl[k] or [r for I in isl for r in I]
parent = parent_select(home, rng)
insp = rng.choice(home)
r = rng.random()
if r < 0.3: # diff：参照父代的最小改动
cand = diff_edit(parent["e"], rng)
elif r < 0.5: # cross：与岛内灵感杂交
cand = cross(parent["e"], insp["e"], rng)
else: # full：整体重写
cand = fresh(rng)
else: # Sample 对照：同预算，无档案复用
cand = fresh(rng)
cand, f = repair(cand, rng) # 有界修复（comp 失败触发，≤2 次）
if f is None:
continue # 编译门：进不了档案
key = canon(cand)
if key in seen: # exact duplicate → EvolAST 强制变异
cand = evolast(cand, rng)
f = comp_ok(cand)
if f is None:
continue
key = canon(cand)
sem = sem_ok(f)
if sem:
hits.add(key)
if key not in seen and sum(len(I) for I in isl) < CAP:
born = rng.randrange(K) if parent is None else next(
i for i in range(K) if any(parent is r for r in isl[i]))
isl[born].append({"e": cand, "sem": sem, "n": 0})
seen.add(key)
if parent is not None:
parent["n"] += 1 # 使用计数（惩罚反复选同一父代）
if t % 10 == 9: # 每 10 代迁移，保护各岛 top-1
for i in range(K):
if len(isl[i]) > 1 and rng.random() < 0.1:
j = (i + 1) % K
elite = max(isl[i], key=lambda r: 1 + r["sem"])
movable = [r for r in isl[i] if r is not elite]
mover = movable[rng.randrange(len(movable))]
isl[i].remove(mover) # 真迁出，不是复制
isl[j].append(mover)
return len(hits), sum(len(I) for I in isl)
if __name__ == "__main__":
# 10 个种子取均值：玩具域里两种方法都只有 0~1 个命中——这本身就是结果（见页内说明）
import statistics as st
fe = [run(True, s) for s in range(10)]
smp = [run(False, s) for s in range(10)]
# Sample 的“档案”只是台账（记录 repertoire，从不复用为父代）
print("FormalEvolve : mean unique sem-OK %.1f / repertoire %.0f" % (
st.mean(h for h, _ in fe), st.mean(a for _, a in fe)))
print("Sample : mean unique sem-OK %.1f / repertoire %.0f" % (
st.mean(h for h, _ in smp), st.mean(a for _, a in smp)))
You are a detective who needs to run a background check on one of
the paper’s authors. Where have they worked? What did they study?
What previous projects might have led to working on this one? What
motivated them to work on this project? Feel free to contact the
authors, but remember to be courteous, polite, and on-topic.
Identify how this paper self-assesses its (likely positive) impact
on the world. Have any additional positive social impacts left out?
What are possible negative social impacts that were overlooked or
omitted?
