TheoremGraph: 형식적 수학과 비형식적 수학을 연결하는 정리 수준 의존성 그래프

왜 중요한가

수학 지식은 정리와 그 의존관계로 구성되며 이를 명시적으로 연결하면 중복 연구를 줄이고 자동화형 추론의 전제 검색을 개선할 수 있다. 기존에는 비형식 논문이 문서 단위로 인용하는 반면 형식 라이브러리는 선언 단위의 정밀한 의존성을 기록해 두 영역이 분리되어 있었다. TheoremGraph는 이 둘을 문장 수준 임베딩과 LLM 판정으로 연결해 형식화·검색·자동정형화(autoformalization) 파이프라인의 문맥 소스를 제공한다.

핵심 기여

대규모 비형식 의존성 그래프 구축

arXiv 수학 논문에서 정리 유사 환경을 정규표현식 기반으로 추출해 11.7M개의 정리 후보를 만들고 여러 추출기(deterministic, heuristic, notation)를 조합해 총 18.3M개의 유향 의존 간선을 복구했다. 각 간선은 제안한 추출기 레이블을 보존해 사용자가 정밀도와 커버리지를 조절할 수 있게 했다. 샘플 500편에 대한 LLM 판정에서 deterministic 추출 간선은 98.8%의 판정 정밀도를 보였다.

LeanGraph를 통한 형식 선언 의존성 추출

Lean 4의 환경 API와 정교한 포함 규칙을 이용해 사용자-가시 선언을 노드로 삼는 선언 수준 그래프를 만들고 25개 프로젝트에서 388,105개 선언과 11.3M개의 유형화된 에지를 추출했다. 에지는 extends, field, sig, proof, def, docref로 분류되어 구조적·타입·값·문서 관계를 분리하여 후속 소비자가 역할별로 필터링할 수 있게 설계되었다. 커널 수준의 후처리된 상수와 증명 항목을 사용해 소스 수준 파서가 놓치는 의존성을 복구했다.

슬로건 임베딩으로 형식-비형식 간 매칭을 성취

각 정리와 선언에 대해 Qwen3-235B 기반 프롬프트 체인으로 만든 문장 요약(slogan)을 생성하고 Qwen3-Embedding-8B로 4096차원 임베딩하여 단일 색인에 넣어 크로스모달 근접검색을 수행했다. 유사도 0.8 이상 후보 100,799건을 GPT-5.4로 판정한 결과 47,952건을 exact 또는 inexact로 확정해 실용적 매칭을 확보했다. 매칭 확률은 유사도 구간에 따라 급상승하며 ≥0.9 구간에서 87%의 판정 동의를 보였다.

표현·검색·그래프 확장으로 MathlibQR 성능 근접

단일 슬로건 임베딩을 이름·시그니처 표현과 결합하고 이름-매칭 인덱스, 쿼리 재작성(HyDE), 이진-HNSW 후보 확대, 의존성 그래프 확장을 순차 적용해 Recall@10을 0.586에서 0.775까지 개선했다. 이 구성은 LeanSearch v2의 reranked Recall@10(0.780)에 0.5pp 이내로 근접했으며 랭킹-최적화 구성은 reranker 없이도 LSv2 retriever를 능가했다. 그러나 동일한 튜닝은 chained-premise 검색(MathlibMPR)에서 성능 저하를 유발해 작업 간 신호 차이가 존재함이 확인되었다.

핵심 아이디어 이해하기

수학적 지식은 정리와 정의 같은 이산적 문장(statement)과 그들 사이의 의존관계로 구성된다. 비형식 논문에서는 인용이 문서 단위로 이뤄져 정밀한 명제 간 연결이 약화되지만, 증명 보조기는 선언 수준에서 모든 의존을 명시적으로 요구해 훨씬 밀도 높은 그래프를 제공한다. 두 영역의 불일치는 자동 검색과 자동정형화 작업에서 중요한 문맥 손실을 초래한다. 문제 해결 원리는 모든 정리와 선언을 동일한 의미 공간으로 사상(mapping)하는 것이다. 구체적으로는 각 문장을 단문 요약(slogan)으로 변환하고 동일한 임베더에 넣어 코사인 유사도로 근접한 정리-선언 쌍을 찾는다. 임베딩 후보군은 이진-HNSW로 빠르게 생성한 뒤 전정밀도 코사인으로 재순위해 유사도 임계치를 넘는 후보만 판정자에게 보낸다. 이 접근은 표면적 어휘 공유가 없어도 의미적으로 동등한 진술을 매칭할 수 있게 한다. 슬로건화가 충분히 정보성 있는 요약을 제공하면 형식 선언과 비형식 정리 사이에 직접적 근접 관계가 생기며, 이 관계는 검색 기반 자동정형화와 의존성 기반 탐색에서 실질적 성능 향상을 가져왔다.

방법론

전체 파이프라인은 네 단계로 조직되었다: 비형식 정리 추출, 형식 선언 추출, 슬로건 생성 및 임베딩, 임베딩 기반 매칭과 LLM 판정이다. 비형식 측은 arXiv LaTeX 원문에서 정리 유사 환경을 정규표현식과 휴리스틱으로 식별하고 내부 참조 처리, 주변 문맥 기반 엣지 생성, 표기법 기반 연결을 수행했다. 각 추출 간선은 제안자 라벨을 보존해 정밀도-커버리지 균형을 사용자가 선택할 수 있게 했다. 형식 측은 Lean 4의 환경(Environment) API에서 후처리된 선언을 노드로 삼아 LeanGraph를 실행했다. 이 과정은 선언을 shouldIncludeConstant 규칙으로 필터링하여 커널 생성 아티팩트를 제거하고 extends/sig/field/proof/def/docref 타입으로 에지를 분류했다. 이로써 타입-레벨 의존성과 값-레벨 의존성 등 역할별 그래프가 구축되었다. 슬로건 생성은 Qwen3-235B 기반의 단계적 프롬프트 체인을 사용해 문장 요약을 얻었다. 먼저 본문만으로 시도하고 실패 판정 시 증명과 로컬 문맥, 이웃 정리와 출구 의존을 순차적으로 추가해 커버리지를 높였다. 생성된 슬로건은 Qwen3-Embedding-8B로 4096차원 임베딩한 뒤 ℓ2 정규화해 코사인을 계산했고 색인에는 pgvector/HNSW가 사용되었다. 매칭 후보는 ann_k로 제어되는 HNSW 후보군에서 얻은 뒤 정밀 코사인으로 재순위하고 유사도 0.8 이상을 모두 GPT-5.4 판정자에게 제출했다. 판정자는 exact·inexact·wrong 세 범주로 분류하며 exact와 inexact를 매칭으로 간주했다. 추가적으로 DeepSeek 같은 느슨한 판정자를 비교군으로 두어 고-정밀과 고-회수 전략을 대조했다.

주요 결과

비형식 파이프라인은 arXiv에서 11.7M개의 정리 유사 환경을 식별하고 총 18.3M개의 후보 의존 간선을 복구했다. 샘플 검증에서 deterministic 추출 간선의 판정 정밀도는 98.8%였고 heuristic과 notation 추출기는 각각 낮은 정밀도와 상호보완적 커버리지를 제공했다. 이 결과는 엣지별 제안자 라벨을 보존함으로써 사용자가 정밀도와 커버리지를 직접 조절할 수 있게 설계되었다. 형식 측에서는 LeanGraph가 25개 프로젝트에서 388,105개의 선언과 11.3M개의 타입화된 에지를 추출했다. 선언-간 밀도는 형식 그래프에서 크게 높았으며 형식 그래프의 에지-대-노드 비율은 약 29.2로 보고되었다. 이 구조화된 그래프는 검색 후 그래프 확장 시 부모 선언을 한 홉 추가하는 식으로 활용되어 개념 단위 검색 성능에 기여했다. 크로스폼 매칭에서는 유사도 0.8 이상 후보 100,799건 중 GPT-5.4 판정으로 47,952건을 exact 또는 inexact 매칭으로 확정해 약 48%의 확정율을 얻었다. 유사도가 높을수록 판정 동의율이 상승해 ≥0.9 구간에서 87%의 확정율을 보였고 DeepSeek 판정자는 더 관대해 61%의 확정율을 기록했다. Retrieval 실험에서 이름·시그니처 표현과 검색-time 기법을 결합한 구성은 MathlibQR fair-810에서 Recall@10을 0.775로 끌어올려 LSv2의 reranked Recall@10(0.780)에 근접했다.

기술 상세

전체 아키텍처는 두 개의 큰 그래프(비형식 정리 그래프, 형식 선언 그래프)와 이를 잇는 공유 임베딩 색인으로 구성된다. 비형식 그래프는 정규표현식 기반 파서와 세 가지 추출기(deterministic, heuristic, notation)를 조합해 정리 노드와 후보 엣지를 생성하고 각 엣지에 추출기 라벨을 붙여 후처리에서 정밀도를 조절할 수 있게 했다. 형식 그래프는 Lean 4의 kernel Environment API에서 후처리된 선언만을 포함하도록 필터링해 노드 집합을 구성하고, 에지는 역할별로 구분해 구조적 분석과 검색 후 확장에 활용할 수 있게 했다. 임베딩 스택은 Qwen3-Embedding-8B(4096차원)를 사용해 각 슬로건을 ℓ2 정규화한 후 pgvector/HNSW 인덱스에 저장하고 후보 생성에는 바이너리-양자화 투영을 적용해 속도를 확보했다. 검색은 ann_k로 제어되는 HNSW 후보군을 얻고 전정밀도 코사인으로 재순위하며 사전정한 임계치(0.8)를 넘는 후보만 판정자로 보낸다. 판정자는 GPT-5.4를 기준으로 엄격하게 exact/inexact/wrong을 반환하도록 설계했고 재실행 검증에서 93.2%의 판정 일관성을 확보했다. 검색-성능 개선을 위해 이름·시그니처를 별도 패시지로 임베딩하고 이름-매칭 인덱스를 추가했으며 쿼리 재작성(HyDE)을 통해 코드형 또는 축약형 쿼리를 슬로건 스타일로 바꿔 검색 호환성을 높였다. 또한 그래프 기반 확장(결과의 formal_dependency 부모 노드 1-hop 추가)은 이름 충돌을 해소하고 개념 수준 검색률을 높였다. 이들 구성은 MathlibQR에서 구성별로 누적 적용되어 Recall과 nDCG 측정치의 변화로 정량화되었다. 평가의 신뢰성 측면에서 블루프린트 쌍을 소스 오브 트루스로 활용해 임베딩 검색이 실제 대응 관계를 회수하는지를 검증했고, 표본 판정과 전문가 재등급화로 판정기 선택(GPT-5.4 채택)을 캘리브레이션했다. 다만 판정은 슬로건과 제한된 문맥만을 참조하므로 더 많은 컨텍스트 제공으로 판정 품질을 끌어올릴 여지가 있다.

한계점

TheoremGraph는 arXiv LaTeX 원문에 의존하므로 모든 수학 저작을 포괄하지 못한다. 비형식 의존성 추출은 휴리스틱과 LLM 보조 단계를 포함해 본질적으로 근사적이며 각 엣지는 제안자 라벨을 통해 정밀도-커버리지 절충을 유지한다. 매칭 판정은 슬로건과 제한된 문맥을 기반으로 이루어져 일부 판정이 실제 동등성을 완전히 보장하지 않을 수 있으며 더 넓은 컨텍스트 제공과 다양한 판정자 평가가 필요하다.

실무 활용

TheoremGraph는 수학 정보 검색, 자동정형화 워크플로, 증명 기반 의존성 탐색에 직접 활용 가능한 인프라를 제공한다. 공개된 API와 MCP 인터페이스는 응용 프로그램과 에이전트가 그래프와 매칭 결과를 실시간으로 조회하도록 지원한다. 단, 데이터 재배포는 원문 라이선스 제약을 따르므로 활용 시 원본 라이선스 필드를 확인해야 한다.

자동정형화(autoformalization) 도구가 비형식 정리에 대해 관련 형식 선언을 탐색해 형식화 스켈레톤을 제안하는 전처리 단계로 사용될 수 있다.
수학 정보 검색 시스템이 이름 기반 질의와 자연어 질의를 병합해 선언을 회수하고, 의존성 그래프 확장으로 관련 전제들을 자동으로 제안하는 파이프라인에 통합될 수 있다.
연구자와 리뷰어가 특정 정리의 의존관계를 추적해 중복 연구 탐지나 인용의정밀성 확인에 활용할 수 있다.

코드 공개 여부: 미확인

키워드

slogan(문장 요약)embedding(임베딩)Lean(Lean 증명 보조기)declaration-level dependency graph(선언 레벨 의존성 그래프)retrieval-augmented formalization(RAG 기반 자동정형화)

용어 해설

문장 요약(슬로건)(Slogan): — 수학 명제를 한 줄 내외의 자연어 문장으로 간결하게 요약한 표현이다. 원문 정리나 정리의 핵심 주장만을 담아 embedding 모델에 입력하기 적합하도록 구성되며, 형식선언과 비형식 서술을 동일한 임베딩 공간으로 매핑하는 관문 역할을 한다. 이 논문에서는 Qwen3 계열 모델로 생성한 slogan을 색인에 저장해 형식/비형식 문장 간 매칭을 수행했다.
슬로건화(Sloganization): — 원문 정리나 선언을 기계가 소비하기 쉬운 짧은 자연어 요약으로 변환하는 절차이다. 단계적 프롬프트 체인을 사용해 본문, 증명, 주변 문맥을 순차적으로 추가하며 실패 시 강제적 대체 문장을 생성하여 커버리지를 높인다. 슬로건화는 서로 다른 표기와 구조를 가진 형식적 선언과 비형식적 문장을 같은 의미 공간으로 투영하는 핵심 전처리 단계이다.
HNSW(근사 최근접탐색)(HNSW): — 대규모 벡터 색인에서 근사 최근접이웃을 빠르게 탐색하는 그래프 기반 알고리즘이다. 삽입 시 다중 레벨의 소근접 그래프를 구성해 탐색 시 이진-근사 후보군을 먼저 얻고, 이후 정밀한 코사인 재평가로 최종 순위를 매긴다. 본 논문에서는 pgvector/HNSW를 후보 생성에 사용하고 양자화 투영을 추가해 색인 효율을 개선했다.
선언 레벨 의존성 그래프(Declaration-level dependency graph): — 증명 보조기에서 컴파일된 선언들 사이의 타입 및 값 차원의 의존관계를 정형화한 방향 그래프이다. 각 노드는 인간이 참조할 수 있는 선언(정의·정리·구조 등)을 나타내고 에지는 sig/extends/field/def/proof/docref 같은 의미론적 유형으로 분류되어 용도에 따라 필터링 가능하다. LeanGraph는 환경 API를 통해 이러한 선언 간 정밀한 의존성을 추출해 대규모 그래프를 구성했다.
Lean 블루프린트(Lean blueprint): — LaTeX 문서에서 각 비형식 명제를 해당 Lean 선언으로 명시적으로 연동한 주석화된 개발 문서이다. 블루프린트는 사람-작성 링크를 제공해 형식·비형식 매칭의 소스 오브 트루스로 작동하며, 논문에서는 이 표본을 통해 임베딩 기반 근접검색이 실제 정답을 회수하는지를 검증했다. 블루프린트 쌍은 자동 매칭의 평가와 캘리브레이션에 사용되었다.

TheoremGraph: 형식적 수학과 비형식적 수학을 연결하는 정리 수준 의존성 그래프

왜 중요한가

핵심 기여

핵심 아이디어 이해하기

방법론

주요 결과

기술 상세

한계점

실무 활용

키워드

용어 해설

관련 토론

댓글

관련 기사

AI가 생성한 코드의 완벽한 정확성을 보장하는 형식 검증과 Lean

왜 중요한가

핵심 기여

핵심 아이디어 이해하기

방법론

주요 결과

기술 상세

한계점

실무 활용

키워드

관련 토론

댓글

관련 기사

AI가 생성한 코드의 완벽한 정확성을 보장하는 형식 검증과 Lean