기술 요약: Ax-Prover

문제 제기

다양한 과학 분야에서 신뢰할 수 있는 형식적 추론이 가능한 대규모 언어 모델 (LLM) 의 개발은 여전히 중요한 과제로 남아 있습니다. 현재 접근 방식은 다음과 같은 이분법에 직면해 있습니다:

1. 전용 증명기 (Specialized Provers): DeepSeek-Prover, Kimina-Prover, Goedel-Prover 와 같은 모델은 Lean 정리 증명에 특화되어 훈련되었습니다. 이들은 수학 경시대회 벤치마크 (예: MiniF2F, PutnamBench) 에서 최첨단 결과를 달성하지만, 일반화 능력은 제한적입니다. 훈련 데이터 외의 분야 (예: 양자 물리학 또는 추상 대수학) 에 적응하는 데 어려움을 겪으며, 진화하는 Mathlib 라이브러리의 업데이트에 취약하여 빈번한 재훈련이 필요한 경우가 많습니다. 또한 외부 도구를 사용하거나 인간 전문가와 상호작용적으로 협력하는 능력이 부족합니다.
2. 범용 LLM: Claude 와 GPT 와 같은 모델은 광범위한 지식과 강력한 추론 능력을 갖추고 있지만, 형식적 증명 도우미와의 네이티브 통합이 부족합니다. 이들은 Lean 환경과 네이티브로 상호작용할 수 없어 접근성은 높지만 엄격하고 기계 검증이 가능한 증명을 생성하지는 못하는 명확한 분열을 초래합니다.

이 격차는 도메인별 재훈련이나 무거운 인프라 없이 범용 LLM 의 광범위한 추론 및 도구 사용 능력과 Lean 의 엄격한 구문적 엄밀성 및 검증 능력을 결합하는 시스템이 필요하게 만듭니다.

방법론

저자들은 Lean 에서 정리 증명을 자동화하도록 설계된 다중 에이전트 에이전트 프레임워크인 Ax-Prover를 소개합니다. 이 시스템은 **모델 컨텍스트 프로토콜 (MCP)**을 활용하여 범용 LLM 에 Lean 도구 세트를 탑재함으로써, 이들이 형식적 환경과 역동적으로 상호작용할 수 있도록 합니다.

시스템 아키텍처

Ax-Prover 는 각 에이전트가 특정 프롬프트를 가진 LLM 인 세 에이전트 워크플로우를 사용합니다:

1. 오케스트레이터 (Orchestrator): 스케줄러 역할을 합니다. 증명되지 않은 정리를 수신하고, Prover 에게 작업을 할당하며, Verifier 로부터의 피드백 라우팅을 관리하고, 개선 루프를 언제 종료할지 결정합니다.
2. Prover: 구성적 핵심입니다. 증명되지 않은 정리를 완성된 증명으로 반복적으로 변환합니다. Prover 는 다음과 같은 점진적 과정을 따릅니다:
   • sorry로 표시된 대상 정리를 식별합니다.
   • 자연어 증명 개요를 생성합니다.
   • 개요를 Lean 문장 ( have 및 sorry 사용) 으로 형식화합니다.
   • sorry 를 대체할 전술 (tactics) 을 제안합니다.
   • 다음 단계로 진행하기 전에 MCP 도구를 사용하여 목표를 검사하고, 보조 정리를 검색하며, 오류를 진단합니다.
3. Verifier: 최종 문지기 역할을 하여 lean diagnostic messages를 사용하여 생성된 Lean 파일을 독립적으로 컴파일합니다. 오류를 보고하고, 증명을 인증하기 전에 sorry 나 레벨 1 오류가 남아있지 않은지 확인합니다.

도구 통합

Ax-Prover 의 핵심 구성 요소는 lean-lsp-mcp 저장소를 통한 Lean 도구 접근성입니다. 이러한 도구를 통해 LLM 은 다음과 같은 작업을 수행할 수 있습니다:

• 파일 관리: .lean 파일을 읽고, 쓰고, 편집합니다.
• 진단: 코드를 컴파일하고 구문 또는 타입 오류를 식별하기 위해 진단 메시지를 검색합니다.
• 컨텍스트 검사: 현재 증명 목표 (lean goal) 와 호버 정보를 쿼리합니다.
• 검색: Mathlib 라이브러리에서 관련 정리 (lean leansearch) 와 타입 서명 (lean loogle) 을 기준으로 선언을 검색합니다.
• 실행: 코드를 실행하고 여러 증명 전략을 시도합니다.

이러한 도구 강화 추론을 통해 Prover 는 계획을 수립하고, 점진적으로 아이디어를 탐색하며, 각 단계에서 정확성을 검증하는 "신중한 수학자"처럼 기능할 수 있습니다.

주요 기여

본 논문은 세 가지 주요 기여를 제시합니다:

1. Ax-Prover 프레임워크: MCP 를 통해 범용 LLM 을 Lean 도구에 연결하는 경량의 에이전트 워크플로우입니다. 이는 도메인별 훈련이나 미세 조정이 필요 없이 수학 및 물리학 전반에 걸쳐 범용 LLM 과 전용 증명기 모두와 동등하거나 더 나은 성능을 보여줍니다.
2. 새로운 벤치마크: 소외된 분야의 형식적 추론을 평가하기 위해 두 개의 새로운 데이터셋을 도입했습니다:
   • AbstractAlgebra: Dummit & Foote 의 교재에서 발췌한 100 개의 문제로, 경시대회 스타일의 퍼즐이 아닌 대학원 수준의 연구 개념 (군, 환, 체) 에 중점을 둡니다.
   • QuantumTheorems: 밀도 행렬, 관측 가능량, 엔트로피 경계 등 기초 양자 역학을 다루는 134 개의 문제로, 이론 물리학과 형식적 검증을 연결합니다.
3. 연구자 친화적 검증: Ax-Prover 를 상호작용형 어시스턴트로 시연합니다. 고전 및 양자 암호학 사례 연구를 통해, 이 시스템은 도메인 전문가와 협력하여 복잡한 보안 보장을 형식화하고 검증함으로써 Lean 전문 지식이 없는 연구자의 진입 장벽을 낮춥니다.

결과

저자들은 Ax-Prover(Claude Sonnet 4 구동) 를 여러 벤치마크에서 전용 증명기 (DeepSeek-Prover-V2-671B, Kimina-Prover-72B) 와 범용 LLM(Sonnet) 과 비교 평가했습니다.

• 새로운 벤치마크 (AbstractAlgebra 및 QuantumTheorems):

  • AbstractAlgebra: Ax-Prover 는 **64%**의 정확도를 달성하여 DeepSeek-Prover(24%) 와 Kimina(13%) 를 크게 앞섰습니다. 전용 모델들은 연구 수준의 대수적 개념이 분포 밖 (out-of-distribution) 이기 때문에 어려움을 겪었습니다.
  • QuantumTheorems: Ax-Prover 는 **96%**의 전체 정확도 (쉬운 문제 100%, 중간 문제 92%) 를 달성한 반면, DeepSeek-Prover 는 61%, Kimina 는 57% 였습니다. 전용 모델들은 표준 Mathlib 에 없는 사용자 정의 물리 정의 (예: bra/ket, 밀도 행렬) 에 일반화하지 못했습니다.
  • NuminaMath-LEAN: Ax-Prover 는 **51%**의 전체 점수를 기록하여 DeepSeek-Prover(28%) 와 Kimina(31%) 를 앞섰으며, 기본 LLM(Sonnet) 은 5% 만 기록했습니다.

• PutnamBench:

  • 이 도전적인 학부생 경시대회 벤치마크에서 Ax-Prover 는 **14%**의 정확도를 달성하여 최고의 오픈소스 모델로 선정되었으며 전체 순위에서는 3 위를 차지했습니다. 92 개의 문제를 해결하여 Goedel-Prover-V2(13%) 와 DeepSeek-Prover-V2(7%) 와 같은 다른 오픈소스 모델을 능가했습니다.
  • 주목할 점은 Ax-Prover 는 전용 모델들이 종종 대규모 병렬 시도 (예: pass@1024) 에 의존하는 반면, pass@1 과 25 분 타임아웃이라는 훨씬 낮은 컴퓨팅 예산으로 이를 달성했다는 것입니다.

• 도구 사용 분석:

  • Prover 는 실행당 평균 약 100 회의 도구 호출을 수행했으며, 높은 성공률 (>99%) 을 보였습니다.
  • Ax-Prover 는 지역적 재작성에 크게 의존한 전용 모델들과 비교하여 더 넓은 범위의 전술 ( change, suffices, norm_cast 포함) 을 활용했습니다. 이는 도구 통합이 창의적 탐색과 사용자 정의 정의 관리 능력을 향상시킨다는 것을 시사합니다.

• 배포 및 비용:

  • Ax-Prover 는 API 접근만 필요로 하는 반면, 전용 모델들은 고성능 GPU 클러스터 (예: H200/A100) 와 MLOps 전문 지식을 요구합니다.
  • Ax-Prover 의 API 비용은 단일 pass@1 시도에서 전용 모델을 실행하는 것보다 높았지만, 경쟁력 있는 성능을 위해 높은 pass@n 값으로 전용 모델을 실행할 때 비용 차이는 크게 축소됩니다 (예: 1000 개의 데이터 포인트에 대해 DeepSeek-Prover 를 pass@1024 로 실행하면 약 307,000 달러가 소요되는 반면 Ax-Prover 는 약 4,000 달러).

중요성과 주장

본 논문은 Ax-Prover 가 훈련 데이터 외의 일반화에 어려움을 겪는 전용 시스템의 한계를 해결하는 다양한 과학 분야에 걸친 형식적 검증을 위한 일반화 가능한 방법론을 제공한다고 주장합니다.

• 일반화: 라이브러리 변경과 도메인 이동에 취약한 전용 증명기와 달리, Ax-Prover 의 도구 기반 접근 방식은 재훈련 없이 새로운 정의 (예: 양자 물리학) 와 진화하는 Mathlib 버전에 적응할 수 있게 합니다.
• 협력: 이 시스템은 AI 와 인간 연구자 간의 격차를 해소합니다. 상호작용형 어시스턴트 역할을 함으로써 도메인 전문가가 깊은 Lean 전문 지식 없이도 형식적 검증에 참여할 수 있게 하며, 암호학 사례 연구에서 비공식적 논증의 미묘한 격차를 식별하는 데 도움을 준 것으로 입증되었습니다.
• 효율성: 이 프레임워크는 비싸고 전용인 인프라의 필요성을 피하면서 "더 간결한" 컴퓨팅 예산으로 경쟁력 있거나 우수한 성능을 달성합니다.

저자들은 Ax-Prover 가 형식적으로 검증된 추론을 통해 과학적 발견에 기여할 수 있는 검증 가능한 과학적 인공지능을 향한 한 걸음이라고 결론지으며, 이는 자율적 정리 증명과 인간-AI 협력 연구를 모두 지원합니다.