AIProver 用证书驱动的 HarnessEvolve 联合进化开放权重 Lean autoformalization 模型与 agent harness

Jana 等提出 AIProver：联合后训练 119B 开放权重模型并用 HarnessEvolve 进化可调用 Lean 工具的 agent harness，把 type correctness、proof completeness 与 semantic correctness 都纳入 verifier certificate。工作同时发布 LoCoBench，含 5.89 万个来自 Mathlib、CSLib、Mizar 与 bounded arithmetic 的实例，其中 771 个验证样本没有公开 Lean 形式化；论文报告在 Leanstral-1.5 基座上 semantic-correct pass@4 从 15.7% 提升到 36.7%，并把同一能力封装成 Claude Code / Codex skill，在对应评测中分别将 semantic correctness 从 41.9% 提升到 79.8%、从 34.1% 提升到 62.4。