Does My Embedding Reflect That \(A = B\)? Evaluating Mathematical Equivalence in Embedding Models

Motivation

• Known: text embedding model은 문서·문장 간 의미적 유사성을 효율적으로 포착하도록 설계되어 있고, LLM들은 이미 연구 수준의 수학 문제 해결에 활용되고 있으며 mathlib 같은 formalization 자원과 arXiv 같은 대규모 수학 문헌 데이터베이스가 계속 성장하고 있다.
• Gap: 그러나 현재의 embedding model들이 표면적 어휘 유사성을 넘어 수학적 동치성(mathematical equivalence) 자체를 포착할 수 있는지에 대한 체계적 평가는 이루어지지 않았으며, 이를 측정할 벤치마크도 부재했다.
• Why: 수학적 동치를 인식하는 embedding model은 대규모 수학 문헌에서 서로 다른 분야(예: 집합론과 범주론)에 걸쳐 동일한 개념을 연결하는 발견을 가능하게 하며, 이는 비용이 큰 LLM 대신 효율적으로 대규모 수학 지식 탐색을 지원하는 핵심 도구가 될 수 있다.
• Approach: 저자들은 어휘적으로 다르지만 수학적으로 동치인 270개 문장 쌍으로 구성된 MELD 데이터셋을 구축해 기존 SOTA embedding model들을 평가하고, mathlib의 formal-informal 다중 view를 활용한 contrastive 학습으로 MathLeap-Qwen-8B와 MathLeap-Octen-8B를 훈련했다.

Achievement

Figure 1. A UMAP visualization of embedded statements from

1. MELD 데이터셋 구축: 9개의 서로 대응되는 수학 하위분야(예: 집합론 vs 범주론, 벡터공간론 vs 모듈론, 표현론 vs 푸리에 해석) 간에 자연어와 LaTeX로 작성된 270개의 수학적으로 동치이나 어휘적으로 상이한 문장 쌍을 Claude Opus 4.7 생성, 수동 검토, GPT-5.5 검증의 파이프라인으로 구축했다.
2. 기존 embedding model의 한계 규명: Qwen3-Embedding-4B/8B, harrier-oss-v1-27b, KaLM-Embedding-Gemma3-12B, llama-embed-nemotron-8b, Octen-Embedding-8B 등 최신 모델들을 MELD로 평가한 결과, 가장 우수한 모델도 Recall@1이 0.241~0.25 수준에 그치고, UMAP 시각화(Figure 1)에서 통계적 동치보다 소속 분야(field)에 따라 클러스터링되는 것을 확인했다.
3. MathLeap 모델 제안 및 성능 개선: mathlib_informal_v4.16.0 데이터셋에 자연어 재구성(rephrasing)을 추가하여 4가지 view(Lean signature, Lean type, 자연어, rephrased 자연어)를 정렬하는 contrastive 학습을 수행한 MathLeap-Qwen-8B와 MathLeap-Octen-8B가 MELD 및 다양한 informal-formal retrieval task에서 기존 모델 대비 최고 성능(Recall@1 27.2~28.9 등)을 달성했다.

How

• MELD 데이터셋 생성: 9개의 상호 대응 도메인 쌍에 대해 두 분야 간 연결성을 설명하는 프롬프트를 Claude Opus 4.7에 제공하여 각 쌍당 30개의 동치 문장 쌍을 생성
• 생성된 문장을 수동으로 검토하여 어휘적 유사성을 낮추면서 수학적 동치성은 유지되도록 수정
• GPT-5.5 (medium)로 (i) 두 문장의 타당성, (ii) 동치 여부, (iii) 유사도를 낮출 수 있는지를 재검증
• 평가: 540개 문장(270쌍)을 여섯 개의 SOTA embedding model로 임베딩하여 Recall@1,3,5,10,20 지표로 동치 쌍 검색 성능 측정, UMAP으로 임베딩 공간 시각화
• MathLeap 학습 데이터 구축: mathlib_informal_v4.16.0의 Lean signature, Lean type, 자연어 설명을 서로 다른 view로 취급
• Qwen3.5-9B로 자연어 정리를 hypothesis와 conclusion으로 명시적으로 분해한 뒤, gemma-4-E4B-it을 이용해 변수명 등 표면적 요소를 바꾼 자연어 재구성(rephrasing)을 추가 생성
• 최종적으로 문장당 3~4개의 view를 가진 118,334개 학습 인스턴스와 15,287개 테스트 인스턴스를 구성
• 이 multi-view 데이터를 이용해 contrastive learning으로 MathLeap-Qwen-8B, MathLeap-Octen-8B를 학습하여 formal-informal 표현 간 정렬을 강화

Originality

• 수학적 동치성(mathematical equivalence)을 어휘적 유사성과 명확히 분리하여 평가하는 새로운 벤치마크(MELD)를 제시한 점이 독창적이며, 특정 수학 하위분야 간 "동일 개념의 다른 관점" 구조(예: 집합론 vs 범주론)를 활용한 데이터 설계가 신선하다.
• formal(Lean)과 informal(자연어) 표현을 동일한 수학적 내용의 서로 다른 "view"로 간주하여 contrastive learning의 positive pair로 활용하는 아이디어는 formalization 자원(mathlib)을 순수 자연어 임베딩 개선에 활용한 새로운 응용이다.
• LLM을 이용한 자동 rephrasing으로 자연어 view의 다양성을 인위적으로 확장해 학습 데이터 규모 문제를 해결한 점도 실용적으로 독창적이다.

Limitation & Further Study

• MELD가 Claude Opus 4.7 생성 및 GPT-5.5 검증에 의존하므로, LLM 생성 데이터 특유의 편향이나 인위적 패턴이 벤치마크에 스며들 위험이 있으며, 270쌍이라는 규모는 통계적 신뢰도 측면에서 제한적이다.
• 본문 발췌에는 MathLeap 모델의 구체적인 contrastive loss 설계, 학습 하이퍼파라미터, 그리고 성능 향상의 근본 원인(단순히 formal-informal alignment 때문인지, 데이터 다양성 증가 때문인지)에 대한 ablation이 명확히 제시되지 않아 인과관계 검증이 부족하다.
• mathlib은 특정 형식화 스타일과 하위분야(주로 순수수학)에 편중되어 있어, 학습된 모델이 다른 수학 분야나 다른 formal system으로 일반화될지는 불확실하며, 이에 대한 후속 연구가 필요하다.
• MELD에 대한 개선(Recall@1 약 28.9%)이 여전히 낮은 수준이어서 근본적인 문제가 완전히 해결되었다고 보기 어렵고, 추가적인 아키텍처적 개선이나 더 큰 규모의 alignment 데이터 확보가 필요하다.

Evaluation

총평: 수학적 동치성 인식이라는 중요하지만 간과되었던 문제를 명확한 벤치마크(MELD)로 드러내고, formalization 자원을 활용한 실용적 해법을 제시한 좋은 워크숍 논문이나, 본문 발췌만으로는 방법론의 세부 검증이 다소 부족해 보인다.