Math-Graph는 워싱턴 대학교 수학인공지능연구소에서 2026년에 공개한 수학 정리 의존성 그래프 데이터셋입니다. 이 데이터셋은 명제 수준의 세분화된 수학 정리 의존성 그래프를 구축합니다. 관련 논문으로는 다음과 같은 것들이 있습니다... TheoremGraph: 형식 수학과 비형식 수학을 연결하는 플랫폼 . 이 데이터셋은 비형식적 수학적 명제와 형식적 수학적 명제 쌍 47,952개를 포함하며, 두 가지 유형의 수학적 지식을 비형식 및 형식 수학 모두를 아우르는 일관된 의존성 그래프로 통합합니다. 데이터셋에는 논문 메타데이터, 수학적 명제(형식/비형식), 의존성 연결선, 그리고 LLM으로 생성된 자연어 설명이 포함됩니다.

데이터셋 구성:

• 비공식 그래프(arXiv): 1,170만 개의 문장 노드와 1,830만 개의 의존성 엣지를 포함하며, 결정론적 규칙, 휴리스틱, 기호 추론, LLM 등 다양한 의존성 추출 방법을 지원합니다.
• 형식 그래프(LeanGraph): 388,000개의 Lean 4 선언 노드와 1,130만 개의 유형이 지정된 종속성 엣지를 포함하며, Mathlib을 포함한 25개 프로젝트를 포괄합니다.

데이터 필드:

• paper_arxiv.csv: arXiv 논문 메타데이터(ID, 제목, 저자, 카테고리, 라이선스, 링크 등 포함).
• paper_lean_community.csv / paper_lean_repo.csv: ID, 제목, 작성자, 카테고리, 라이선스, 링크 등을 포함한 Lean 프로젝트 메타데이터입니다.
• statement_informal.csv / statement_formal.csv: 진술/선언 내용, 유형, 위치, 컨텍스트 및 라이선스 게이트 필드.
• informal_dependency.csv / formal_dependency.csv: 문장, 추출 방법, 유형 및 참조 위치 간의 방향성 종속성입니다.
• slogan.csv: 각 문장에 대한 자연어 슬로건, 프롬프트 단어 버전, 모델 구성 및 토큰 사용량을 기록합니다.

소환

@misc{kurgan2026theoremgraph,
title         = {TheoremGraph: Bridging Formal and Informal Mathematics},
author        = {Kurgan, Simon and Wang, Evan and Leonen, Eric and Szeto, Sophie and
Alexander, Luke and Remizov, Artemii and Alper, Jarod and
Inchiostro, Giovanni and Ilin, Vasily},
year          = {2026},
eprint        = {2606.25363},
archivePrefix = {arXiv},
primaryClass  = {cs.IR},
url           = {https://arxiv.org/abs/2606.25363}
}