Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis

이 논문은 자연어 수학 명제를 Lean 4 형식 언어로 자동 변환하는 과정에서 발생하는 근본적인 문제를 해결하기 위해 제안된 도구 증강 에이전트 (Tool-Augmented Agents) 프레임워크에 대한 체계적인 연구입니다. 저자들은 LLM 의 확률적 특성과 형식 수학의 엄밀성 사이의 괴리를 해소하기 위해 반복적 개선 (Iterative Refinement) 을 가능하게 하는 에이전트 아키텍처를 설계하고, 3 가지 주요 도구 범주 (정교화된 모델 쿼리, 지식 검색, 컴파일러 피드백) 의 효과를 계량화하기 위해 **요인 분석 (Factorial Analysis)**을 수행했습니다.

주요 내용은 다음과 같습니다.

1. 문제 정의 (Problem Setting)

• 배경: 대규모 언어 모델 (LLM) 은 복잡한 수학 논증을 생성할 수 있지만, 확률적 특성은 형식 수학이 요구하는 절대적인 확실성과 충돌합니다.
• 현황: Lean 4 와 같은 증명 보조기기는 논리적 정확성을 기계적으로 검증하지만, "형식화 병목 현상 (Formalization Bottleneck)"으로 인해 대부분의 대학원 수준 수학 정리는 자연어로만 존재하고 형식화되지 않았습니다.
• 기존 방법의 한계:
  • 할루시네이션: 학습 데이터가 부족하여 존재하지 않는 정리나 심볼을 생성합니다.
  • 의미 불일치: 집합론적 직관 (교과서) 과 Lean 의 의존형 이론 (Dependent Type Theory) 간의 깊은 불일치로 인해 직접 번역이 어렵습니다.
  • 구문 vs 의미: 코드가 컴파일되더라도 (구문 오류 없음) 논리적으로 빈약하거나 잘못된 명제일 수 있습니다.
  • 동적 환경: Mathlib 4 는 빠르게 진화하는 라이브러리이므로, 정적 스냅샷으로 학습된 모델은 폐기된 정의나 존재하지 않는 심볼을 참조하는 코드를 생성합니다.

2. 방법론 (Methodology)

저자는 정적 생성을 반복적 개선으로 대체하는 에이전트 프레임워크를 제안했습니다.

• 아키텍처: 중앙 LLM 오케스트레이터 (GPT-5.2) 가 Lean 4 환경과 상호작용하며, 상태 유지와 행동 결과 관찰을 통해 다음 단계를 결정합니다.
• 3 가지 도구 범주 (Tool Categories):
  1. 전문가 초안 작성 (Expert Drafting): 미세 조정된 모델 (Herald) 을 통해 전문적인 번역 초안을 제공합니다.
  2. 지식 검색 (Knowledge Search): lean inspect name 등을 통해 Mathlib 에서 심볼의 실제 정의와 타입을 검색합니다.
  3. 컴파일러 피드백 (Compiler Feedback): Lean REPL 을 통해 코드를 실행하고 정밀한 오류 메시지를 받아 구문 및 유효성 문제를 반복적으로 수정합니다.
• 실험 설계:
  • 데이터셋: 실해석, 복소해석, 위상수학, 대수학 등 4 가지 수학 분야에서 추출한 400 개의 대학원 수준 정리.
  • 평가 프로토콜: 1 단계 컴파일 성공 여부 확인, 2 단계 LLM 심사관 (GPT-5.2) 을 통한 의미적 동등성 (Faithfulness) 평가 (0~10 점, 9 점 이상을 'Faithful'로 간주).
  • 요인 분석 (Factorial Analysis): 3 가지 도구의 유무 (2^3 = 8 가지 구성) 를 조합하여 각 도구의 주효과 (Main Effect) 와 상호작용 효과를 정량화했습니다.

3. 주요 결과 (Key Results)

• 성능 향상:
  • One-shot Baseline: 컴파일 성공률 약 26%, 의미적 정확도 (Faithfulness) 약 10~28% 에 그쳤습니다.
  • Full Tool-Augmented Agent: 컴파일 성공률 89.5%, 의미적 정확도 **60.5%**로 크게 향상되었습니다.
• 요인 분석 결과 (가장 중요한 통찰):
  • 컴파일러 피드백 (Feedback, F): 성능 향상의 **가장 결정적인 요인 (+32.3 점)**입니다. REPL 을 통한 반복적 수정이 에이전트를 저성능 영역에서 고성능 영역으로 전환시켰습니다.
  • 검색 (Search, S): 안정화 요인 (+6.8 점) 으로 작용합니다. 할루시네이션을 줄이고 이름 해결을 돕지만, 피드백 루프가 활성화된 상태에서는 그 효과가 감소합니다 (피드백이 심볼 검색의 역할을 대체함).
  • 전문가 초안 (Translation, T): 대체 가능한 요소 (+0.9 점) 입니다. 오케스트레이터 모델이 이미 강력하고 피드백/검색이 존재할 경우, 외부 초안 작성 모델의 추가 이점은 미미하거나 오히려 방해가 될 수 있습니다.
• 상호작용 효과:
  • 피드백 (F) 이 있을 때 검색 (S) 을 추가하면 컴파일 시도 횟수가 줄어들어 효율성이 향상되지만, 최종 정확도에는 큰 변화가 없습니다.
  • 피드백이 없는 상태에서는 검색이 큰 효과를 발휘하지만, 피드백이 있는 상태에서는 검색의 역할이 정보 수집 방식의 전환 (시행착오 감소) 으로 바뀝니다.
• 도메인별 분석: 복소해석은 가장 적은 반복으로 해결되는 반면, 실해석은 가장 많은 계산 오버헤드가 필요했습니다.

4. 기여 및 의의 (Contributions & Significance)

• 구조적 통찰: 형식화 성공의 핵심은 모델의 파라미터적 전문성 (Fine-tuning) 이 아니라, **실행 환경 (Execution Environment) 과 검색 (Retrieval)**의 결합임을 증명했습니다.
• 설계 원칙 제안: 형식 추론 에이전트 설계 시, 고정된 오프라인 초안 작성자보다는 **고정밀 실행 환경 (컴파일러 피드백) 을 주된 지지대 (Scaffold)**로 삼고, 검색을 통해 수렴을 안정화하고 가속화하는 접근이 효과적입니다.
• 지속 가능성: 빠르게 진화하는 형식 라이브러리 (Mathlib) 에서는 정적 데이터셋에 대한 일회성 미세 조정보다는 **검증과 결합된 반복 (Verification-coupled iteration)**이 더 중요합니다.
• 오픈소스 및 재현성: 벤치마크, 에이전트 구현, 평가 스크립트, 그리고 에이전트의 도구 호출 로그 (RL 학습을 위한 귀중한 데이터셋) 를 공개하여 향후 연구를 지원합니다.

5. 결론

이 연구는 자연어 수학 형식화 분야에서 LLM 이 겪는 한계를 도구 증강 에이전트를 통해 극복할 수 있음을 보여주었습니다. 특히 컴파일러 피드백 루프가 형식화의 정확성을 보장하는 가장 강력한 메커니즘이며, 이는 추후 형식 수학 자동화 시스템 설계의 핵심 원칙이 될 것입니다.