Astra 기반 mini-Lean-agent가 Putnam 문제 12개를 풀었다

Lean 정리 증명 에이전트가 Putnam 2025 문제 12개를 모두 풀었습니다. 모델에 보이는 도구는 명령창 하나였고, Astra를 기반 모델로 쓴 실험에서 문제당 평균 비용은 1.28달러였습니다. 저는 전용 도구를 여러 겹 쌓지 않은 구성이 이 결과를 냈다는 점이 오래 남습니다.

Mingbird는 작은 로컬 모델의 작업 완수를 돕는 에이전트 하네스(agent harness)를 만듭니다. mini-Lean-agent는 Lean 증명 작업에서 도구를 명령창으로 단순화합니다. 두 사례 모두 에이전트의 결과를 모델 성능만으로 설명하기보다 작업 흐름과 검증 방식을 함께 보게 합니다.

mini-Lean-agent는 일반 코딩 에이전트의 단순한 작업 방식으로 정리 증명 문제를 풉니다. 에이전트가 만든 최종 증명은 별도의 신뢰된 평가기가 검증합니다. 도구를 간단하게 두면서도 정답 판정은 에이전트의 자기 보고에 맡기지 않는 점이 반갑습니다.

다만 12개 완주는 Astra를 기반 모델로 쓴 결과이고, 다른 모델에서는 수치가 달랐습니다. Gemini 3.8 Flash에 문제당 2달러 한도를 둔 실험은 12개 중 7개를 풀었습니다. 같은 조건의 AxProverBase는 4개를 풀었습니다. 1.28달러의 평균 비용과 12개 완주를 다른 모델이나 예산 조건의 성능으로 옮겨 읽으면 차이가 사라집니다.

Lean 에이전트를 비교하신다면 같은 12문제를 대상으로 모델과 문제당 비용 한도를 고정한 뒤 에이전트 구성만 바꿔 보십시오. 문제별 해결 여부와 실제 비용, 별도 평가기의 검증 결과를 함께 기록하면 성공 수가 늘어난 이유를 살필 수 있습니다.

에이전트 성능을 비교하실 때, 같은 모델로 도구 구성을 비교하는 일과 같은 도구로 모델을 비교하는 일 가운데 무엇부터 하시겠습니까?