기술 요약: ProofWala

문제 정의

신경망 방법을 이용한 자동 정리 증명(Automated theorem proving)은 인터랙티브 정리 증명기(ITP)와 상호작용하기 위한 견고한 인프라, 구조화된 증명 데이터 추출, 그리고 대규모 증명 탐색을 실행할 수 있는 환경을 필요로 한다. 기존의 도구들은 파편화되어 있고, 특정 어시스턴트에 종속되어 있으며, REPL(Read-Eval-Print Loop) 인터페이스를 통한 인터랙티브한 파일 단위 실행에 치중되어 있다. 이러한 아키텍처는 다음과 같은 중대한 한계를 지닌다:

• 확장성: 이는 저장소 규모의 분석과 병렬 실험을 저해한다.
• 데이터 추출: 선언 수준의 메타데이터(예: 귀납적 정의, 상수, 네임스페이스)에 대한 접근을 제한하며, 저장소 전역의 의존성 그래프를 구축하는 것을 어렵거나 불가능하게 만든다.
• 교차 어시스턴트 간의 격차: 통일된 도구의 부재는 다국어 형식 코퍼스(예: Lean 및 Rocq)를 통한 학습에서 얻을 수 있는 잠재적인 교차 언어 및 교차 도메인 이득을 활용하는 것을 어렵게 만든다.

방법론

저자들은 서로 다른 ITP 간의 상호작용, 데이터 추출, 학습 및 탐색을 통합하도록 설계된 다국어 증명 엔지니어링 프레임워크인 ProofWala를 제시한다. 이 프레임워크는 세 가지 핵심 구성 요소를 중심으로 구축되었다:

1. 인터페이스 모듈 (itp-interface)

이는 ITP와 프로그래밍 방식으로 상호작용하기 위한 재사용 가능한 라이브러리로, Lean 4와 Rocq(여러 버전)에 대한 통일된 추상화를 제공한다.

• Lean 4 백엔드: REPL 기반 아키텍처에 의존하는 대신, 저자들은 Lean 엘라보레이터(elaborator) 내부에서 직접 실행되는 **메타 프로그램(meta-programs)**을 구현하였다. 이를 통해 다음이 가능하다:
  • 의미론적으로 충실한 택틱(tactic) 수준의 트레이싱(tracing).
  • 선언 수준의 메타데이터 추출 및 저장소 전역의 의존성 그래프 구축.
  • 중첩된 택틱 구조(예: have 블록)의 개선된 처리.
  • 환경 클로닝(Environment Cloning): 표준 REPL 워크플로우에서는 어려운, 병렬 실행을 위한 증명 환경 클로닝 능력.
  • 버전 견고성: 4.15.0부터 시작하는 Lean 4 버전들에 대한 순방향 호환성을 보장하는 얇은 호환 계층.
• Rocq 백엔드: coq_serapy를 기반으로 구축되었으며, 이를 확장하여 증명 상태와 택틱 트레이스를 체계적으로 추출하고 이를 Lean에서 사용되는 것과 동일한 통합 형식으로 매핑한다.
• 통합 상태 모델: 두 어시스턴트는 증명 상태가 의무 사항(목표 및 가설)의 집합이고 택틱이 이러한 상태를 전이시키는 표준화된 상태 전이 시스템으로 매핑된다.

2. 데이터 및 모델 모듈

• 데이터 추출: 프레임워크는 어시스턴트의 커널 내부에서 택틱 스크립트를 재생함으로써 주요 저장소(CompCert, MathComp, GeoCoq, Mathability, CategoryTheory)로부터 증명 상태-택틱 쌍을 추출한다.
• 통합 형식: 추출된 데이터는 의미론적 정보를 보존하면서도 어시스턴트별 세부 사항을 추상화하는 통합된 JSON 형식으로 저장된다. 학습을 위한 프롬프트 형식은 Lean과 Rocq 간의 교차 어시스턴트 학습을 용이하게 하기 위해 어시스턴트 특정 토큰을 생략하여 동일하게 구성된다.
• 학습: 저자들은 CodeT5-Base 모델(220M 파라미터)을 다음 세 가지 구성으로 미세 조정(fine-tuning)하였다:
  1. ProofWala-Rocq: Rocq 저장소로 학습됨.
  2. ProofWala-Lean: Lean 저장소로 학습됨.
  3. ProofWala-Multilingual: 두 어시스턴트 모두에서 공동 학습됨.

3. 병렬 증명 탐색 모듈

• 환경 풀(Environment Pool): 핵심적인 혁신은 동일한 프런티어 상태로 초기화된 여러 개의 클론된 증명 환경을 유지하는 환경 풀이다.
• 병렬 실행: 후보 택틱들은 이러한 클론된 인스립스(instances)들 사이에서 동시에 실행된다. 이 풀은 분산 실행을 위해 Ray와 통합되어, 확장 가능한 증명 탐색과 대규모 주석 생성(annotation)을 가능하게 한다.
• 탐색 알고리즘: 이 모듈은 병렬화된 최선 우선 탐색(best-first search) 및 빔 탐색(beam search)을 지원한다. 유효하고 컴파일 가능한 상태 전이만을 기록하는 주석이 달린 증명 트리를 유지하여, 탐색 역학에 대한 미세한 분석을 가능하게 한다.

주요 기여

1. 표준화된 프레임워크 및 엔지니어링 라이브러리: ProofWala는 택틱 수준의 데이터를 추출하고 조직하며 도구 개발을 지원하는 통합 프레임워크를 제공한다. 이는 REPL을 통해 달성하기 어려웠던 의존성 인식 저장소 순회 및 환경 클로닝 기능을 지원하는 Lean용 메타 프로그래밍된 인스트루멘테이션(instrumentation) 파이프라인을 도입한다.
2. 병렬 증명 완성을 위한 지원: 이 프레임워크는 명시적으로 클론된 증명 환경과 통합된 다중 ITP 인터페이스 내에서의 동시 택틱 평가를 지원함으로써 병렬 증명 탐색을 제공하는 최초의 오픈 소스 시스템이다.
3. 다국어 데이터셋 및 모델: 저자들은 엔드 투 엔드 증명 탐색을 용이하게 하는 다국어 데이터셋(약 45만 개 데이터 포인트, 2억 7천만 토큰)과 학습된 모델(Lean, Rocq, 및 Multilingual)을 공개한다.

결과

저자들은 CompCert, MathComp, GeoCoq, CategoryTheory, Lean/Mathlib의 테스트 분할 및 MiniF2F 벤치마크에서 모델을 평가하였다.

• 교차 언어 전이: ProofWala-Multilingual 모델은 일반적으로 단일 언어 베이스라인과 대등하거나 이를 능가한다.
  • 통계적으로 유의미한 개선: 가장 큰 벤치마크(Lean/Mathlib)와 CategoryTheory 도메인 적응 설정(CategoryTheory 데이터로 다국어 모델을 미세 조정한 경우)에서 관찰되었다.
  • 경향성: 다른 데이터셋에서도 다국어 학습을 선호하는 일관된 경향을 보였으나 통계적으로 유의미하지는 않았다.
• 도메인 적응: CategoryTheory 도메인에서 다국어 모델은 Rocq 전용 베이스라인에 비해 미세 조정 후 현저히 높은 pass-at-k 점수를 달성하였으며, 이는 혼합 언어 데이터로 사전 학습하는 것이 대상 도메인이 하나의 어시스턴트로만 표현된 경우에도 적응을 돕는다는 것을 시사한다.
• 탐색 역학: 증명 트리 분석 결과, 다국어 모델은 종종 더 큰 트리와 더 높은 분기 계수(branching factor)를 생성하는 것으로 나타났다. 이는 모델이 상태당 더 많은 유효한 택틱을 제안함을 의미한다.
• 확장성: 환경 풀을 통한 병렬 실행은 처리량을 크게 향상시켰다. CPU 워커를 8개에서 20개로 늘렸을 때, MiniF2F의 pass@5가 22.54%에서 26.23%로 향상되는 동시에 평균 증명 시간은 단축되었다.

의의 및 주장

본 논문은 ProofWala가 파편화되고 특정 어시스턴트에 국한된 도구에서 신경 증명(neural theorem proving)을 위한 통합되고 확장 가능한 인프라로의 전환을 나타낸다고 주장한다.

• 아키텍처 통합: 실행, 데이터 수집, 의존성 분석 및 탐색을 통합함으로써, 이 프레임워크는 다중 ITP에 걸친 신경 증명의 체계적이고 재현 가능하며 미세한 분석을 가능하게 한다.
• 전이의 증거: 본 연구는 다국어 학습이 형식적 추론에서 교차 언어 및 교차 도메인 전이를 유발한다는 실증적 증거를 제공하며, 특히 고데이터(high-data) 환경과 도메인 적응 시나리오에서 그러하다.
• 연구 기반: 저자들은 ProofWala를 단순한 증명 탐색 시스템이 아니라, 증명 탐색을 "블랙박스" 평가에서 분석 가능한 파이프라인으로 변모시키는 연구 프레임워크로 정의한다. 이를 통해 연구자들은 이전에는 얻기 어려웠던 방식의 구조적 전이, 트리 크기, 분기 계수 및 실행 지연 시간을 연구할 수 있다.

저자들은 최첨단 성능을 위해 더 큰 모델과 추가적인 인프라(예: 검색, 검증기)가 필요할 수 있다고 언급하면서도, 그들의 주요 기여는 다국어 학습과 병렬 탐색 전략의 효과를 분리하여 보여주는 프레임워크 자체에 있다고 강조한다. 또한, 문서 지향적 어시스턴트(Isabelle 등)로의 확장은 개념적 한계라기보다 엔지니어링 과제이며, 이를 향후 연구 과제로 남겨둔다.