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

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

수학적 지식은 정리와 정의 같은 이산적 문장(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 보조 단계를 포함해 본질적으로 근사적이며 각 엣지는 제안자 라벨을 통해 정밀도-커버리지 절충을 유지한다. 매칭 판정은 슬로건과 제한된 문맥을 기반으로 이루어져 일부 판정이 실제 동등성을 완전히 보장하지 않을 수 있으며 더 넓은 컨텍스트 제공과 다양한 판정자 평가가 필요하다.