형식적 정리 증명 (Formal Theorem Proving)을 위한 올바른 대칭성은 무엇인가?

대규모 언어 모델 (LLMs) 기반의 형식적 정리 증명기 (Formal theorem provers)는 문제 표현의 표면적인 변화에 매우 민감합니다. 즉, 의미론적으로 동일한 문장이라도 증명 성공률이 극명하게 다르게 나타날 수 있으며, 이는 형식적 수학에 내재된 구조적 대칭성 (structural symmetries)을 존중하지 못함을 드러냅니다. 이는 다음과 같은 핵심적인 질문을 제기합니다: 형식적 정리 증명을 위한 올바른 대칭성은 무엇인가? 본 논문에서는 증명 전술 (proof tactics)에 의해 유도되는 구성적이고 일반적으로 가역적이지 않은 변환을 포착하는 범주론적 프레임워크 (category-theoretic framework)인 재작성 범주 (rewriting categories)를 도입하고, 이를 사용하여 두 가지 대칭 개념을 정식화합니다: 재작성에 따라 증명 분포가 어떻게 변하는지를 규정하는 증명 등변성 (proof equivariance), 그리고 동등한 문장들이 동일한 확률로 해결되어야 함을 요구하는 성공 불변성 (success invariance, 즉 성공 확률의 불변성)입니다. 우리는 상태 기반 차기 전술 증명기 (state-based next-tactic provers)가 증명 상태 (proof states)를 기반으로 작동함으로써 자연스럽게 증명 등변성을 만족한다는 것을 관찰했습니다. 반면, 최첨단 LLM 기반 증명기들은 두 속성을 모두 만족하지 못하며, 동등한 공식화 사이에서 큰 성능 차이를 보입니다. 이를 완화하기 위해, 우리는 입력의 동등한 재작성들에 대해 집계하는 테스트 시간 (test-time) 방법론을 제안하며, 이 방법론이 샘플링 한계 (sampling limit) 내에서 성공 불변성을 회복한다는 것을 이론적으로 보여주고, 고정된 추론 예산 (inference budgets) 하에서 강건성 (robustness)과 성능을 향상시킨다는 것을 실증적으로 보여줍니다. 우리의 결과는 대칭성이 LLM 기반 정리 증명에서 결여된 핵심적인 귀납적 편향 (inductive bias)임을 강조하며, 이를 근사하기 위한 실질적인 경로로서 테스트 시간 연산 (test-time computation)을 제안합니다.