Non-Parametric Structural Priors for Geometry Theorem Prediction

Motivation

• Known: 기존 neural-symbolic geometry problem solving(GPS) 파이프라인은 신경망이 후보 정리를 제안하는 정책 역할을 하고 symbolic solver가 상태를 관리하는 구조로, supervised parametric model이 in-distribution에서 높은 정확도를 달성해왔다. 또한 LLM을 Lean, Isabelle 등 formal language의 planner로 사용하는 연구와 RAG/GraphRAG 기반 검색 증강 추론 기법들이 존재한다.
• Gap: supervised parametric model은 고정된 theorem set에 대해서만 학습되어 새로운 혹은 확장된 theorem library에 대한 일반화가 어렵고 재학습 비용이 크며, vanilla ICL은 추론 깊이가 늘어날수록 잠재적 위상적 의존관계(latent topological dependency)를 복원하지 못해 근사적으로 균등한 행동 분포를 보이며 unstructured exploration과 오류 누적으로 급격히 성능이 저하되는 Structural Drift 문제가 존재한다.
• Why: gradient 기반 재학습 없이도 LLM이 구조적 사전지식(structural prior)을 활용해 복잡한 symbolic reasoning 문제에서 supervised 모델에 필적하는 성능을 낼 수 있음을 보임으로써, 진화하는 theorem library에 유연하게 적응 가능한 training-free reasoning 패러다임의 가능성을 제시한다.
• Approach: 과거 solution trace들로부터 정리 간 선후 관계를 encoding한 방향 그래프인 Theorem Precedence Graph를 retrieval-augmented 방식으로 문제별로 동적 구성하고, 이를 명시적 위상 제약(topological constraint)으로 LLM 프롬프트에 결합하여 LLM이 stepwise symbolic executor와 상호작용하는 structured planner로 동작하게 한다.

Achievement

Figure 1. Geometry problem solving accuracy (%) across reason-

1. Structural Drift 현상 규명: 추론 깊이(L1-L6)가 증가할수록 vanilla ICL의 정확도가 급격히(일부는 거의 0으로) 저하되는 현상을 정량적으로 확인하고, 이를 LLM의 잠재적 위상 의존성 복원 실패로 귀속시켰다.
2. Pri-TPG 프레임워크 제안: Theorem Precedence Graph를 통한 비매개변수적(non-parametric) 구조적 사전지식 주입으로 gradient 기반 최적화 없이 검색 공간을 효과적으로 pruning했다.
3. FormalGeo7k 벤치마크에서 89.29% 정확도 달성: ICL baseline 대비 큰 폭의 성능 향상(예: L5, L6에서 각각 +58.1%, +23.3% 향상)을 보였으며, state-of-the-art supervised model과 견줄만한 성능을 training-free 방식으로 달성했다.

How

Figure 2. Overview of our Pri-TPG workflow, where we successively refine the structural prior to provide precise guidanc

• 기하 문제를 P = (T, D, S0, g) 튜플로 정형화하고 theorem 적용 시퀀스가 symbolic precondition을 만족하며 목표 상태에 도달하는 constrained symbolic planning 문제로 공식화
• 과거 solution trace로부터 정리 간 시간적 선후 관계를 추출해 directed graph 형태의 Theorem Precedence Graph(TPG)를 구성
• retrieval-augmented 전략을 사용해 입력 문제에 조건화된 TPG를 즉석에서(on the fly) 동적 생성
• LLM이 동적 TPG가 부여한 위상적 제약 하에서 다음 정리를 제안하는 planner 역할을 수행하고, symbolic solver가 executor로서 상태 전이의 유효성을 검증 및 실행
• FormalGeo7k benchmark에서 vanilla ICL baseline 및 supervised neural approach와 비교 실험 수행

Originality

• Structural Drift라는 새로운 실패 모드를 명명하고 추론 깊이에 따른 ICL 성능 저하를 체계적으로 규명한 점
• content-augmented RAG에서 structure-augmented reasoning으로의 전환을 제안하여, 검색된 콘텐츠 자체에 명시적 구조(directed precedence graph)를 부여한 최초의 접근
• RL 기반 alignment 없이도 과거 solution trace로부터 "planning intuition"을 직접 추출할 수 있음을 보인 non-parametric 접근법

Limitation & Further Study

• 초기 symbolic state S0가 이미 주어진다는 가정 하에 theorem prediction에만 집중하고 있어, 실제 end-to-end formalization 과정의 어려움은 다루지 않음
• TPG가 과거 solution trace에 의존하므로, 완전히 새로운 유형의 문제나 trace가 부족한 도메인에서는 성능 저하 가능성이 존재하며 이에 대한 분석이 제한적일 수 있음
• FormalGeo7k라는 단일 벤치마크에 대한 검증으로, 다른 formal reasoning 도메인(Lean, Isabelle 등)으로의 일반화 가능성에 대한 추가 검증이 필요함
• retrieval 품질에 대한 의존성 및 대규모 theorem library에서의 확장성(scalability)에 대한 심층 분석이 후속 연구로 필요함

Evaluation

총평: Structural Drift라는 명확한 문제를 제시하고 이를 non-parametric한 Theorem Precedence Graph로 해결하는 참신하고 실용적인 접근으로, training-free 방식으로 supervised 모델에 필적하는 성능을 보인 점이 인상적이나 단일 벤치마크 검증의 한계가 있다.