Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

기술 요약: 서지학적 지식과 형식화된 수학적 지식 사이의 가교 계층을 향하여

문제 정의
현대의 수학적 지식은 현재 두 개의 구조적으로 독립된 인프라에 파편화되어 있다. 한쪽에는 MathSciNet이나 zbMATH Open과 같은 서지 데이터베이스가 있어, 인간이 읽을 수 있는 연구 기록을 색인화하고 출판 메타데이터, 인용 네트워크, 전문가 리뷰를 포착한다. 다른 한쪽에는 Lean의 mathlib과 같은 형식 증명 라이브러리와 대화형 정리 증명기(ITP)가 존재하며, 이는 기계적으로 검증 가능한 수학을 형식적으로 체크된 객체로 인코딩한다. 이 생태계들은 상호 보완적이지만 서로 단절되어 있다. 즉, 서지 시스템은 결과물이 형식화되었는지 여부를 나타내지 않으며, 형식 라이브러리는 출판 메타데이터가 아닌 내부 의존성 그래프를 중심으로 구성된다. 고전적 결과와 기계화된 발전을 매핑하는 "정렬 아티팩트"(설문 논문이나 문서화 등)가 존재하기는 하지만, 이러한 매핑은 파편화되어 있고 표준화되지 않았으며, 질의 가능한 계층으로 체계적으로 통합되지 않았다.

방법론
본 논문은 기존의 인프라를 대체하지 않으면서 이를 통합하도록 설계된 **관계형 브리지 데이터베이스(relational bridge-database)**를 제안한다. 핵심 방법론은 세 가지 구성 요소로 이루어진다:

1. 아키텍처 통합: 이 시스템은 서지 기록(MathSciNet 및 zbMATH Open)을 형식적 아티팩트(Lean, Reservoir 등)와 연결하는 정렬 인프라로서 기능한다. 이는 새로운 동료 검토나 형식 검증을 수행하는 것이 아니라, 출판물과 형식 코드 간의 대응 관계를 기록하는 아카이브 플랫폼 역할을 한다.
2. 형식화 점수 ($S(P_i)$): 저자들은 특정 논문 $P_i$의 형식화 정도를 측정하기 위한 정량적 지표를 정의한다.
   • 논문은 수학적 문장들 $S_i$(정의, 보조정리, 정리, 추측 등)의 집합으로 취급된다.
   • 각 문장 $s$에 대해 이진 지표 $\phi(s)$가 할당된다: $s$가 Lean에서 완전히 형식화되었다면 1, 그렇지 않으면 0이다.
   • 요구 사항의 구분:
     • 순수 문장(정의, 구성, 추측)은 형식적 객체의 존재만을 요구한다.
     • 증명된 문장(정리, 보조정리)은 형식적 문장과 완전한 형식적 증명을 모두 요구한다.
   • 점수는 다음과 같이 계산된다: $S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$.
3. 교차 문서 정렬을 통한 타당성 연구: 이러한 점수를 대규모로 추정할 수 있음을 입증하기 위해, 저자들은 제로샷(zero-shot) 설정에서 대규모 언어 모델(LLM)을 활용하였다. 모델은 비형식적 수학 논문(PDF 1)과 형식화 문서 또는 Lean 구현체(PDF 2)를 비교하는 과업을 수행했다. 모델은 다음을 수행하도록 지시받았다:
   • 비형식적 텍스트에서 세밀한 수학적 문장을 추출한다.
   • 이를 "순수(Pure)" 또는 "증명됨(Proved)"으로 분류한다.
   • 형식적 텍text 내에서 의미론적 대응 관계를 식별한다.
   • 매칭된 문장의 비율을 기반으로 형식화 점수를 계산한다.

주요 기여

• 상호운용성 계층: 출판 메타데이터를 형식 코드 저장소와 연결하여 서지 레지스트리와 형식 검증 환경을 통합하는 데이터베이스 제안.
• 형식화 점수 정의: 출판물의 형식 시스템 내 커버리지를 정량화하는 엄격한 논문 수준의 지표($S(P_i)$)를 정의하며, 정의의 존재와 증명의 존재를 구분함.
• 타당성 입증: LLM이 비형식적 텍스트와 형식적 아티팩트를 정렬함으로써 이러한 점수를 성공적으로 추정할 수 있음을 보여주는 개념 증명 연구.

실험 결과
저자들은 Google Gemini를 사용하여 미세 조정 없이 6개의 수학 논문에 대한 실험을 수행하였다. 결과는 다양한 형식화 정도를 구별하는 시스템의 능력을 입증하였다:

• 높은 커버리지: 8차원 구 패킹(sphere packing) 문제는 100점을 받아 완전한 형식화를 나타냈다.
• 부분적 커버리지: $\zeta(3)$의 무리성에 관한 논문과 다중 등급(multi-graded) Proj 스킴 관련 논문은 각각 50점과 67.74(두 번째 실험에서는 96.30)를 기록하여, 상당 부분 형식화되었으나 불완전함을 반영했다.
• 낮음/없음 커버리지: "Dilatations of categories"에 관한 논문은 41.67을 받았고, "Algebraic magnetism"에 관한 서베이 논문은 관련 없는 문서와 매칭되었을 때 0을 받았다(해당 논문은 Lean 구현체가 없음).
• 실험을 통해 모델이 관련 형식화가 존재하지 않을 때 이를 정확히 식별할 수 있으며, 완전히 형식화된 작업과 부분적으로 형식화된 작업을 구분할 수 있음을 확인하였다.

의의 및 주장
본 논문은 이 연구를 서지학적 체계와 형식적 수학 생태계를 확장 가능한 기계 실행 가능 지식 그래프로 통합하기 위한 첫 단계로 규정한다. 저자들은 제안된 시스템이 기존의 출판 또는 검증 인프라를 대체하는 것이 아님을 명시한다. 대신, 이는 기존의 비형식적인 정렬 지식을 구조화되고 질의 가능한 자원으로 체계화하는 "연결 계층" 역할을 한다.

이 연구의 의의는 다음과 같다:

1. 출판된 결과와 그에 대응하는 형식적 객체에 대한 통합된 접근 제공.
2. 수학 문헌 중 얼마나 많은 부분이 형식화되었는지에 대한 대규모 분석 가능.
3. 출판물을 형식적 증명 객체와 연결하는 토대를 마련하여, 향후 AI 생성 수학 및 인간-AI 하이브리드 워크플로우를 지원할 잠재력 보유.

저자들은 PDF 파싱이 모호성을 유발하고, 검색 품질이 점수 정확도에 영향을 미치며, LLM이 허위 대응 관계를 생성할 수 있다는 점을 언급하며 한계를 인정하였다. 따라서 이들은 본 시스템을 완벽한 매핑을 위한 도구가 아닌, 관계적 정렬을 위한 "최선 노력 프레임워크(best-effort framework)"로 정의하며, 향-후 하이퍼링크와 매핑이 현재의 서지 관행과 유사하게 수동으로 큐레이션되거나 지도 학습 프로세스를 통해 이루어질 것으로 기대하고 있다.