13,920개 노드 기반 Graph Search를 통한 수학적 증명 자동화 시스템 구축

Context

무한한 수학적 문장 탐색으로 인한 기존 증명 자동화의 계산 복잡도 한계 발생. 단순한 텍스트 기반 탐색 대신 기성의 증명 기법과 공리를 연결하는 구조적 접근 필요성 증대.

Technical Solution

• 수학적 증명을 Axiom $\rightarrow$ Technique $\rightarrow$ State $\rightarrow$ Theorem으로 이어지는 Directed Graph의 Path-finding 문제로 재정의
• 12개 Technique Cluster와 정형화된 Signature(Input, Process, Output, Precondition)를 통한 Search Space의 유한 구조화
• Orchestrator LLM이 Scoring Heuristic을 기반으로 기법을 선택하고 Worker LLM이 병렬로 적용하는 계층적 추론 아키텍처 설계
• 불가능성 정리(Impossibility Theorems)를 기준으로 유효하지 않은 경로를 즉시 제거하는 Pruner 도입을 통한 탐색 효율 최적화
• 서로 다른 도메인을 연결하는 Cross-field Transfer 기법에 가중치를 부여하여 새로운 증명 발견 가능성 제고

Impact

• 13,920개 Total Nodes 및 23,397개 Directed Edges로 구성된 고밀도 지식 그래프 구축
• 3,791개 Axiom, 4,994개 State, 4,262개 Theorem, 873개 Technique 노드를 통한 구조적 증명 경로 확보

Key Takeaway

비정형의 무한한 탐색 공간을 정형화된 기술 시그니처와 그래프 구조로 변환하여 LLM의 추론 범위를 제한하고 정확도를 높이는 제약 기반 설계(Constraint-based Design)의 효용성 확인.