비모수적 구조적 사전 지식을 활용한 다단계 정리 예측

On Multi-Step Theorem Prediction via Non-Parametric Structural Priors

다단계 정리 예측은 자동 추론의 핵심적인 과제입니다. 기존의 신경-기호 접근 방식은 지도 학습 기반의 매개변수 모델에 크게 의존하며, 이는 변화하는 정리 라이브러리에 대한 일반화 능력이 제한적입니다. 본 연구에서는 문맥 내 학습(ICL) 관점에서 학습이 필요 없는 정리 예측 방법을 탐구합니다. 우리는 중요한 확장성 병목 현상인 '구조적 드리프트(Structural Drift)'를 발견했습니다. 추론 깊이가 증가함에 따라, 기본적인 ICL의 성능이 급격히 저하되어, 종종 거의 0에 가까워집니다. 이러한 실패는 LLM이 잠재적인 위상적 의존성을 복구하지 못하여 구조화되지 않은 탐색을 수행하기 때문이라고 판단했습니다. 이 문제를 해결하기 위해, 우리는 '정리 선행 그래프(Theorem Precedence Graphs)'를 제안합니다. 이는 과거 해결 과정의 기록을 기반으로 시간적 의존성을 방향 그래프로 인코딩하고, 추론 과정에서 검색 공간을 효과적으로 줄이는 명시적인 위상적 제약을 적용합니다. 검색 증강 그래프 구성 및 단계별 기호 실행기와 결합하여, 우리의 접근 방식은 LLM이 기울기 기반 최적화 없이도 구조화된 계획기로 작동할 수 있도록 합니다. FormalGeo7k 벤치마크에서 수행한 실험 결과, 제안하는 방법은 89.29%의 정확도를 달성하여, ICL 기반의 기존 방법보다 훨씬 우수하고, 최첨단 지도 학습 모델과 동등한 성능을 보였습니다. 이러한 결과는 명시적인 구조적 사전 지식이 LLM 기반 기호 추론의 확장성을 향상시키는 유망한 방향임을 시사합니다.

Multi-step theorem prediction is a central challenge in automated reasoning. Existing neural-symbolic approaches rely heavily on supervised parametric models, which exhibit limited generalization to evolving theorem libraries. In this work, we explore training-free theorem prediction through the lens of in-context learning (ICL). We identify a critical scalability bottleneck, termed Structural Drift: as reasoning depth increases, the performance of vanilla ICL degrades sharply, often collapsing to near zero. We attribute this failure to the LLM's inability to recover latent topological dependencies, leading to unstructured exploration. To address this issue, we propose Theorem Precedence Graphs, which encode temporal dependencies from historical solution traces as directed graphs, and impose explicit topological constraints that effectively prune the search space during inference. Coupled with retrieval-augmented graph construction and a stepwise symbolic executor, our approach enables LLMs to act as structured planners without any gradient-based optimization. Experiments on the FormalGeo7k benchmark show that our method achieves 89.29% accuracy, substantially outperforming ICL baselines and matching state-of-the-art supervised models. These results indicate that explicit structural priors offer a promising direction for scaling LLM-based symbolic reasoning.