기술 요약: Lean에서의 에이전틱 정리 증명기(Agentic Theorem Prover)의 비용-품질 트레이드오프 최적화

문제 정의

대규모 언어 모델(LLM)은 에이전틱 워크플로우를 채택함으로써 Lean 증명 보조 도구 내에서의 자동 정리 증명 분야에서 상당한 진전을 이루었습니다. 이러한 워크플로우는 일반적으로 복잡한 문제를 더 작은 보조 정리(lemma)로 분해하고, 수많은 증명 시도를 생성하며, 컴파일러 피드백을 활용하여 탐색을 유도합니다. 이러한 방식은 PutnamBench와 같은 도전적인 벤치마크에서 높은 성능을 발휘하지만, 막대한 계산 비용을 초래합니다. 현재의 시스템들은 난이도와 상관없이 분해 및 증명 생성에 고정된 사전 지정 예산을 할당하는 "고정 단계(fixed-step)" 정책을 사용합니다. 이러한 정책은 에이전트가 실현 불가능한 문제나 성공 가능성이 낮은 오형식화된 문장에 과도한 컴퓨팅 자원을 소비하게 함으로써 상당한 낭비를 초래합니다. 핵심 과제는 기존 에이전트들이 결여하고 있는 동적 비용 인지 능력이며, 이는 계산 지출과 증명 성공률 사이의 트레이드오프를 최적화하지 못합니다.

방법론

저자들은 정적 정책을 대체하기 위해 설계된 새로운 액션 라우팅 에이전트(Action Routing Agent) 아키텍처를 제안합니다. 이 시스템은 개념적으로 두 개의 평면으로 나뉩니다.

1. 데이터 평면 (증명 생성)

이전 연구(예: Chen et al., 2025c; Varambally et al., 2025)에서 영감을 받은 데이터 평면은 실제 증명 생성을 처리합니다. 이는 네 가지 모듈을 통해 작동합니다:

• 분해 모듈(Breakdown Module): 범용 모델(GPT-OSS-20B)이 원래의 문제를 자연어 보조 정리와 증명 스케치로 분해합니다.
• 형식화기(Formalizer): 에이전트는 GOEDEL-FORMALIZER-V2-8B를 사용하여 이 보조 정리들을 Lean 코드로 형식화하며, 구문 또는 타입 오류 없이 컴파일되는 최적의 후보를 선택합니다.
• 형식적 분해 증명기(Formal Breakdown Prover): 시스템은 자연어 스케치에 따라 형식화된 보조 정리들을 공리(axioms)로 사용하여 상위 레벨 정리를 증명하려고 시도합니다.
• 보조 정리 증명기(Lemma Prover): 분해가 증명되면, 에이전트는 증명에 필요한 개별 보조 정리들을 증명하기 위해 재귀적으로 시도하며, 새로운 의존성들을 스택에 쌓습니다.

2. 제어 평면 (비용-품질 라우팅)

제어 평면은 실패한 증명 시도의 궤적(trajectory)을 관찰하고, 현재 타겟을 계속 시도할지 아니-면 현재의 분해 방식을 폐기하고 새로운 분해 방식으로 재시작할지를 결정합니다. 이는 비용-품질 트레이드오프를 기반으로 하는 경량 라우팅 정책을 활용합니다:

• 상태($s$): 증명 시도, 컴파일 결과, 에러 메시지, 출력 길이를 포함한 실패한 시도 이력을 요약합니다.
• 액션 공간(Action Space): $\{ \text{ATTEMPT}, \text{TERMINATE} \}$. 에이전트는 현재 타겟에 대해 다른 증명을 샘플링하거나, 현재의 분해 방식을 폐기합니다.
• 유틸리티 함수: 라우터는 $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$를 계산합니다:
  • $\hat{q}(s)$는 다음 시도의 예상 성공 확률(품질)입니다.
  • $\hat{c}(s)$는 다음 시도의 예상 비용(LLM 생성 토큰/SFLOPs로 측정)입니다.
  • $\lambda$는 계산 비용에 대한 페널티를 조절하는 하이퍼파라미터입니다.
• 결정 규칙: 만약 $\tau(s) > 0$이면 에이전트는 계속 진행하고, 그렇지 않으면 현재 궤적을 종료합니다.

추정기(Estimators):

• 비용 추정기: 시도 비용이 독립 항등 분포(i.i.d.)를 따른다고 가정하며, 궤적 내 이전 시도들의 평균 비용을 사용합니다.
• 품질 추정기: 궤적 특징을 기반으로 성공 확률을 예측하도록 훈련된 로지스틱 회귀 모델이며, 구체적인 특징은 다음과 같습니다:
  • 증명 유사도(Proof Similarity): 정규화된 증명들의 평균 쌍별 퍼지 문자열 비율(낮은 유사도는 혼란을 시사함).
  • 에러 다양성(Error Diversity): 고유한 컴파일 에러와 전체 에러 간의 비율(낮은 다양성은 지속적인 실패 모드를 시사함).
  • 시도 횟수(Attempt Count): 이전 시도 횟수.

주요 기여

1. 비효율성 식별: 본 논문은 Lean 에이전트에서 고정 단계 스케일링이 매우 비효율적이며, 불필요한 시도를 줄이는 것이 더 나은 비용-품질 트레이드오프를 위해 필수적임을 식별했습니다.
2. 새로운 아키텍처: 온라인 적응형 비용-품질 라우터를 갖추어 추가 계산의 한계 효용을 동적으로 평가하는 보조 정리 스타일의 Lean 증명기를 개발했습니다.
3. 실증적 검증: 제안된 라우터가 경쟁력 있는 정확도를 유지하면서도 불필요한 계산을 크게 줄인다는 것을 입증하여, 실패한 궤적이 자원 할당을 위한 실행 가능한 신호를 포함하고 있음을 증명했습니다.

실험 결과

시스템은 PutnamBench의 85개 문제 중 일부를 대상으로 고정 단계 베이스라인 및 정답 성공 확률에 접근할 수 있는 "오라클(oracle)" 에이전트와 비교하여 평가되었습니다.

• 비용 절감: 동일한 정확도 수준에서, 제안된 에이전트는 고정 단계 베이스라인에 비해 필요한 예산을 평균 25.8% 감소시켰습니다.
• 정확도 향 향상: 동일한 비용 수준에서, 에이전트는 해결률(solve rate)을 7.8% 개선했습니다.
• 구체적 트레이드오프:
  • 약 43.6%의 해결률을 달기 위해 고정 단계 베이스라인은 31.6 M SFLOPs가 필요했던 반면, 라우팅 에이전트는 22.6 M SFLOPs만 필요했습니다 (28.4% 비용 절감).
  • 중간 규모 예산 체제(약 41.6% 해결률)에서 에이전트는 비용을 29.6% (17.5 M vs. 24.9 M SFLOPs) 줄였습니다.
• 절제 연구(Ablation Studies):
  • 특징 중요도: "에러 다양성"이 품질 추정을 위한 가장 중요한 특징인 것으로 나타났습니다.
  • 데이터 평면 영향: 보조 정리 스타일의 분해 아키텍처 자체가 동일한 8B 모델을 사용하는 전체 증명 생성 방식보다 해결률을 거의 100% 향상시켜, 32B 모델의 성능에 근접하게 만들었습니다.
  • 오라클 격차: 라우팅 에이전트가 고정 베이스라인보다 크게 우수했지만, 59.9%의 비용 절감을 달성한 오라클 에이전트와는 여전히 격차가 존재하며, 이는 특징 공학 및 추정기 아키텍처의 개선 여지를 시사합니다.

의의 및 주장

본 논문은 실패한 Lean 궤적이 비용 인지적 자원 할당을 위한 실행 가능한 신호를 제공한다고 주장합니다. 정적, 고정 단계 정책에서 벗어나 동적 라우팅으로 전환함으로써, 에이전트는 성능을 희생하지 않고도 계산 낭비를 크게 줄일 수 있습니다. 저자들은 이 연구를 "비용 인지 제어(cost-aware control)"를 향한 기초적인 단계로 위치시키며, 미래의 에이전트는 추론 예산을 정적으로 할당하기보다 관찰된 진전과 실패 패턴에 따라 계산을 동적으로 할당해야 한다고 제안합니다. 결과는 고정 단계 정책이 효율성 개선을 위한 상당한 여지를 남겨두고 있으며, 라우팅 전략이 불필요한 비용을 효과적으로 완화할 수 있음을 보여줍니다.