Maith: Lean의 elaborated Expr 트리에서 IR을 추출해 토큰화하는 실험적 프로젝트

이 요약은 AI가 원문을 분석해 생성했습니다. 정확한 내용은 원문 기준으로 확인하세요.

TL;DR

형식 증명에서 LLM 성능이 낮은 원인으로 소스 텍스트의 표면적 잡음을 지목하고, Maith는 Lean의 elaborated Expr 트리에서 직접 IR을 추출해 이를 정규화한 뒤 토큰화하는 방식을 구현했다. 초기 실험에서 Mathlib.Algebra.Group.Defs의 1,129개 선언 중 792개(70%)를 성공적으로 추출했고 337개(30%)는 주로 HOF 적용과 projection 관련 실패로 분류되었다. mul_assoc나 DivisionMonoid.mk 같은 비단순 선언은 잘 처리되어 의미론적 구조 보존 가능성이 확인되었으나 아직 LM 훈련이나 raw-source 토큰화와의 비교 실험은 이루어지지 않았다. 따라서 다음 단계로 모델 학습과 직접 비교를 통해 정규화된 IR의 실효성과 elaboration 의존성으로 인한 비용 대비 효과를 평가할 필요가 있다.

주요 논점

01찬성다수

표면 텍스트 대신 elaborated Expr 기반 IR을 토큰화하면 의미론적 잡음을 줄여 모델이 더 직접적인 수학적 구조를 학습할 수 있다는 주장이다.

02중립다수

Expr 기반 접근은 초기 추출 성공률(70%)로 실현 가능성을 보였으나 완전한 성공을 위해 HOF 및 projection 처리 개선이 필요하다는 입장이다.

03반대소수

정규화된 IR가 일부 유용한 표면 신호를 제거해 오히려 모델 성능을 저해하거나, Lean의 elaborator 의존성으로 실용성·이식성이 떨어질 수 있다는 우려이다.

합의점 vs 논쟁점

합의점

Expr 트리에서 직접 IR을 추출하는 접근이 기술적으로 실현 가능하며 일부 비단순 선언을 잘 처리한다는 점에는 동의가 형성되어 있다.
현재의 실패 원인들은 구체적이며 HOF 적용과 projection 처리에 집중된 만큼 개선 여지가 존재한다는 점에도 공감대가 형성되어 있다.
원본 소스 기반 토큰화와의 정량적 비교가 수행되기 전까지는 최종 결론을 도출하기 어렵다는 점에서 의견이 일치한다.

논쟁점

정규화 과정에서 제거되는 표면적 구문 정보가 모델 학습에 긍정적 영향만 주는지 또는 중요한 신호를 잃게 하는지 여부가 논쟁거리이다.
Lean의 elaboration 의존성이 실환경 배포와 도구 체인 복잡도 측면에서 정당화되는지에 대한 견해가 분열되어 있다.
Expr 기반 토큰화의 적용 범위를 얼마나 넓은 수학 라이브러리까지 확장할 수 있는지, 즉 실패율을 충분히 낮출 수 있는지에 대한 불확실성이 존재한다.

실용적 조언

실험적 비교를 위해 동일 구조의 모델과 동일한 학습 설정으로 raw-source 토큰화와 Expr 기반 토큰화를 직접 비교하는 실험 설계를 우선할 필요가 있다.
실패 사례(HOF, projection 등)를 재현 가능한 소형 테스트셋으로 분류하고 각 케이스에 대해 canonicalization 규칙을 단계적으로 추가해 커버리지 개선 효과를 측정해야 한다.
Elaboration 의존성으로 인한 설치·운영 비용을 줄이기 위해 추출 파이프라인을 독립 실행형으로 패키징하거나 실패 시 graceful fallback으로 소스 기반 토큰화를 병행하는 전략을 고려할 수 있다.

섹션별 상세

LLM이 형식적 정리 증명에서 성능이 낮게 관찰되는 원인 중 하나로서 토큰화 대상의 선택을 지목하고 있다. 원문 소스는 표기법, 암시적 인수, 매크로 같은 구문적 요소가 남아 있어 모델 입력이 표면적 잡음으로 가득하다는 점이 문제로 지적되었다. 이 문제를 해결하기 위해 Maith는 소스 텍스트 파싱을 건너뛰고 Lean의 elaboration 단계 후 생성되는 Expr 트리에서 직접 IR을 추출해 토큰화하는 방식을 채택했다.

Maith가 동작하는 방식은 Lean의 elaborated Expr 구조를 가져와 이를 정규화한 뒤 토큰 단위로 변환하는 파이프라인이다. 구현 상태는 빌드와 전체 테스트 스위트가 통과했고 실제 추출을 Mathlib.Algebra.Group.Defs 모듈(1,129개 선언)을 대상으로 실행해 792개 성공(70%)과 337개 실패(30%)라는 실측치를 확보했다. 비단순 선언들인 mul_assoc나 DivisionMonoid.mk 같은 항목은 제대로 추출되어 의미론적 구조가 보존됨이 확인됐다.

현재 실패 원인은 주로 고차 함수(HOF) 적용과 projection 표현식 등 elaboration 상의 특정 구조에서 발생하는 것으로 분류되어 있다. 이러한 실패 모드는 Expr 기반 추출에서 처리해야 할 케이스가 명확히 존재함을 보여주며, 실패를 줄이기 위한 보정 로직과 canonicalization 규칙 확장이 필요하다. 실패 원인 분류가 존재하므로 향후 실패 케이스별로 재현 가능한 수정 경로를 설계할 수 있다.

아직 훈련된 언어 모델 실험이나 원본 소스 기반 토큰화와의 직접 비교는 진행되지 않아 성능 우위의 결론은 보류 상태이다. 다음 단계로 LM을 학습시키고 raw-source 토큰화와 비교 실험을 수행할 계획이라고 밝혀졌으며, 이 과정에서 elaboration 의존성이 가져오는 설치·운영 비용과 이득의 균형을 평가하려는 의도가 드러난다. 핵심 실무적 질문은 구문을 정규화해 의미 중심 IR을 쓰는 편이 모델 학습·추론에 실질적 이득을 주는가와 그 대가로서 도입되는 종속성의 비용을 어떻게 상쇄할 것인가이다.

용어 해설

Elaboration: — Lean에서 표면 문법에 포함된 암시적 인수와 매크로 등이 구체적인 표현식으로 변환되는 과정으로, 소스 텍스트에 남지 않는 의미적 정보를 생성하며 이 정보를 이용하면 모델 입력에서 잡음을 줄일 수 있다.
Expr tree: — Lean 내부에서 표현식을 계층적 노드 구조로 표현한 자료구조로서 식별자, 응용(application), 람다, 타입 정보 등이 구조적으로 보존되어 모델에 더 직접적이고 의미론적 입력을 제공할 수 있다.
Canonicalization: — 구문적 변형과 등가 표현을 일관된 표준 형태로 바꾸는 처리로서, 다양한 표기법과 매크로를 동일한 내부 표현으로 통일해 토큰 분포를 단순화하고 모델 학습 안정성을 높이는 목적이 있다.
Tokenization: — 소스나 내부 표현을 모델이 처리할 단위로 분할하는 과정으로, 어떤 단위를 토큰으로 삼느냐에 따라 입력의 잡음 수준과 학습 효율이 크게 달라지며 본 게시물에서는 소스 텍스트 기반 대신 Expr 기반 토큰화를 실험하고 있다.
Mathlib: — Lean 생태계의 표준 수학 라이브러리로서 대규모 정리들과 선언들을 포함하며, 자동화 및 추출 파이프라인의 범위와 난이도를 평가하는 실제 코퍼스 역할을 한다.

언급된 도구

Maith중립링크

Lean의 elaborated Expr 트리에서 IR을 추출하고 이를 정규화·토큰화하는 실험적 도구

Lean중립

형식화된 정리와 증명을 작성하는 정리증명기이며 elaboration 단계에서 표현식 트리를 생성하는 역할

Mathlib중립

Lean 생태계의 표준 수학 라이브러리로서 추출 파이프라인의 실험 대상 코퍼스를 제공

언급된 리소스

GitHubMaith GitHub 저장소