# 自进化AI智能体应与基准共同进化

- 来源：elvis (@omarsar0)
- 发布时间：2026-07-22 22:05
- AIHOT 分数：41
- AIHOT 链接：https://aihot.virxact.com/items/cmrw69k6600enro8g7onudka9
- 原文链接：https://x.com/omarsar0/status/2079930722232754623

## AI 摘要

论文提出一种自进化Lean证明智能体，通过可信运行时包裹可变工作区，让智能体重写证明分解、编译器反馈利用和错误修复流程。经过15代进化，该智能体在miniF2F上达到45.1%的保留求解率，远超固定基准智能体的32.0%和初始版本的12.7%。

## 正文

I agree with what this AI paper suggests.

Self-improving agents should evolve their benchmarks too.

（bookmark it）

Self-improving agents are one of the most important directions in AI right now， and most of them optimize against a fixed benchmark. This paper argues the benchmark should evolve alongside the agent.

The setup is a self-evolving Lean proof agent. A small trusted runtime wraps a fully mutable workspace of workflow， prompts， and tools， so the agent can rewrite how it decomposes proofs， uses compiler feedback， and repairs failures.

What makes it different is coevolution. Between generations the champion revises the active task distribution through a mastery-throttled curriculum that adds harder proof obligations only after the current level is mastered.

All of it stays inside a Lean-grounded loop， so a success counts only when the behavior yields verified proofs under a trusted snapshot. Over 15 generations the best coevolving agent reaches 45.1% held-out solve rate on miniF2F， versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent.

Grounding every reward in a formal verifier is how you get self-modification without reward hacking， and coevolving the curriculum pushes the ceiling higher.

Paper： https://arxiv.org/abs/2607.17352

Learn to build effective AI agents in our academy： https://academy.dair.ai/