Self-Supervised Theorem Discovery in a Formal Axiomatic System

Motivation

• Known: 기존 수학적 추론 AI 시스템(LLM 포함)은 수학 텍스트, 코드, 정리 library 등 인간이 구축한 사전 지식에 크게 의존하여 높은 성능을 달성해왔다. 또한 axiom으로부터 학습하는 일부 선행 연구(Wu et al., 2021; Poesia et al., 2024; Kasriel et al., 2025 등)는 axiomatized domain에서 agent가 self-improve하며 정리나 증명을 발견할 수 있음을 보였다.
• Gap: Kasriel et al. (2025)와 같은 선행 연구는 axiom으로부터 정리를 발견하고 LLM judge로 유용성을 평가했지만, 그렇게 발견된 정리가 실제로 외부 reasoning agent(예: LLM)의 증명 성능을 lemma로서 향상시킬 수 있는지는 검증되지 않았다. 즉, 인간이 제공한 정리 library 없이 순수하게 axiom과 추론 규칙만으로 발견한 정리가 human mathematical 관점에서, 그리고 외부 시스템에 실질적으로 유용한지는 열린 질문이었다.
• Why: 인간이 제공한 사전 지식 없이도 agent가 자율적으로 유용한 수학 지식을 발견할 수 있는지는 self-evolving AI 시스템의 근본적 질문이며, 형식 체계(formal axiomatic system) 안에서 이를 검증함으로써 발견된 지식이 형식적으로 검증 가능(formally verifiable)한 채로 수학을 위한 자기진화형 AI로 나아가는 경로를 제시한다는 점에서 중요하다.
• Approach: 명제 논리를 위한 Hilbert axiom system에서 proof search를 stack-machine decision process로 정식화하고, proof search와 useful-theorem extraction을 번갈아 수행하며 발견된 정리를 lemma(theorem action)로 재사용하는 self-supervised theorem-discovery algorithm을 제안한다.

Achievement

Figure 4. Number of discovered theorems in the Hilbert axiom

1. 대규모 정리 발견: 제안된 agent는 axiom과 Modus Ponens만으로 시작해 수만 개(tens of thousands)의 정리를 스스로 발견한다.
2. 인간 벤치마크 문제 해결: 발견된 정리 library를 활용해 인간이 작성한 benchmark 문제들에 대한 증명을 찾아내, 발견된 정리들이 human mathematical 관점에서도 의미 있음을 시사한다.
3. LLM 증명 성능 향상: 발견된 정리를 prompt lemma로 제공했을 때 외부 LLM의 증명 성능이 향상되어, 이 정리들이 LLM reasoning을 위한 external knowledge로 기능할 수 있음을 보인다.

How

Figure 3. An example proof-search episode used to generate goals and training data. Marked states are single-formula sta

• 명제 논리 formula를 →와 ⊥만으로 구성하고, 나머지 연결사(¬, ∧, ∨, ↔)는 이들의 syntactic sugar로 정의
• Ax1, Ax2, Ax3와 Modus Ponens로 구성된 Hilbert system을 채택하고, proof search를 state가 현재 proof stack이고 action이 axiom을 push하거나 Modus Ponens를 적용하는 stack-machine decision process로 정식화
• proof search 중 도달한 formula를 정리 후보로 간주하고, 이를 향후 proof의 goal로 재사용하는 goal-conditioned policy를 자기 자신의 성공적 proof prefix(action sequence)로부터 self-supervised 방식으로 학습
• 발견된 정리 집합에서 useful theorem을 추출하여 theorem action으로 추가함으로써, 이후 세대(generation)의 proof search에서 lemma로 재사용 가능하도록 library를 점진적으로 확장
• proof search와 useful-theorem extraction을 반복(alternate)하는 self-supervised theorem-discovery algorithm으로 통합

Originality

• 기존의 axiom-기반 자기개선 연구들과 달리, 발견된 정리가 external LLM의 실제 proof 성능을 향상시키는지를 직접 검증한 최초의 시도
• 인간이 제공한 theorem library, proof corpus, natural-language prior, 심지어 훈련용 problem set조차 전혀 사용하지 않고 오직 axiom과 추론 규칙만으로 시작하는 극도로 minimal한 setting을 설계
• propositional Hilbert system의 proof 구성을 stack-machine decision process로 재정식화하여 강화학습/self-supervised 학습 프레임워크에 자연스럽게 결합
• proof search와 theorem extraction을 alternating하며 반복적으로 library를 성장시키는 self-supervised 루프 설계

Limitation & Further Study

• 명제 논리(propositional logic)의 Hilbert system이라는 매우 제한적이고 단순한 형식 체계에서만 검증되어, 1차 논리나 고차 수학 이론 등 더 복잡한 axiomatic system으로의 확장 가능성은 미지수
• coNP-complete인 propositional validity 문제 특성상 search space가 커질수록 확장성(scalability) 문제가 발생할 수 있어, 더 복잡한 정리에 대한 discovery 성능은 추가 검증 필요
• "useful theorem" 추출 기준이 human benchmark와의 매칭이나 proof search 성공률에 의존하는데, 이 기준 자체가 얼마나 일반화 가능한 유용성 척도인지에 대한 심층 분석이 부족
• 후속 연구로는 1차 논리, 집합론, 산술 등 더 표현력이 풍부한 axiomatic system으로의 확장, 그리고 발견된 정리의 인간 해석 가능성(interpretability) 및 수학적 의미 분석이 필요

Evaluation

총평: 인간 사전지식 없이 순수 axiom으로부터 유용한 정리를 자율적으로 발견하고 이를 외부 LLM 증명 성능 향상에까지 연결한 점에서 self-evolving mathematical AI 연구에 중요한 실증적 근거를 제공하는 흥미로운 workshop 논문이다. 다만 propositional logic이라는 제한된 setting에서의 검증이라는 점에서 더 복잡한 형식 체계로의 일반화 여부가 향후 핵심 과제로 남는다.