Step-Level Elaboration Improves Natural Language Verification of Research-Level Mathematical Proofs

Motivation

• Known: LLM 및 agent 프레임워크는 수학 문제 풀이(problem-solving)에서는 인상적인 성과를 보이나, Lean 등 formal verification 시스템은 Mathlib 같은 수작업 라이브러리에 의존해 확장성이 제한된다. 따라서 natural language 상에서의 증명 검증은 여전히 중요한 미해결 영역으로 남아있다.
• Gap: 기존 global evaluation 방식은 표면적으로 그럴듯한 문장이 미묘한 논리적 결함을 가리는 "context poisoning" 문제를 겪어, hallucination(거짓 수용) 또는 over-skepticism(과도한 거부)으로 이어진다. 또한 verification을 direct judgment로 다루면 LLM 내부 판단이 opaque하여 오류 국소화(localization)가 어렵다.
• Why: research-level 수학 증명에 대한 신뢰할 수 있는 natural language 검증 능력은 agent가 스스로 탐색적 추론 과정에서 잘못된 경로를 가지치기(pruning)하고 hallucinatory하거나 구조적으로 결함 있는 증명 생성을 줄이는 데 핵심적이며, 향후 automated proof-review agent 개발에도 중요한 함의를 갖는다.
• Approach: direct anomaly detection 대신, 증명을 순서화된 deduction step (s1,...,sn)으로 분해하고 각 step을 (Γi, Σi, Ti) 삼분 구조(내부 맥락, 외부 지식, 배경 이론)로 출처를 명시하며 constructive elaboration을 시도하는 state-driven agentic workflow를 설계한다.

Achievement

1. False acceptance 제거: FirstProof challenge 기반 21개의 research-grade 증명으로 구성된 curated adversarial diagnostic suite에서, 강력한 baseline도 속아 넘어가는 구조적으로 정교한 pseudoproof에 대해 제안 프레임워크는 zero false acceptance를 달성했다.
2. 오류 분류 체계의 근본적 전환: 오류 분석 결과, 남은 rejection은 심각한 logical hallucination이 아니라 명시되지 않은 domain convention에서 비롯된 "pedantic hyper-rigor"가 대부분임을 밝혀, 오히려 expert benchmark 자체에 내재된 암묵적 모호성을 드러냈다.
3. Ablation을 통한 구성요소 검증: constructive step-level elaboration과 외부 수학적 출처(source)에 대한 통제가 미묘한 논리 오류를 국소화하는 데 필수적임을 체계적 ablation study로 입증했다.

How

• 증명 텍스트 S를 문자열로 취급해 논리적 주장을 포함하는 deduction step들의 순서열 (s1, s2, ..., sn)로 분해
• 각 step si를 더 세밀한 파생 문자열 s'i로 elaboration하되 원 추론 궤적을 보존하면서 내재된 논리를 명시적으로 풀어냄
• 각 step의 논리적 의존성을 (Γi: internal context, Σi: external knowledge, Ti: background theory)의 tripartite architecture로 모델링해 정리(theorem) 사용 출처를 명시적으로 통제
• 고정된 prompt file로 안내되는 autonomous state-driven agentic workflow 구현: 각 step은 기본적으로 open(local) 상태로 시작, 반복적으로 elaboration을 시도해 verified 또는 flawed로 전이
• flawed로 표시된 step에는 고정된 confirmation phase를 적용해 재평가 시 open으로 되돌릴 수 있도록 하여 pedantic over-rejection(false positive)을 방지
• 엄격한 halting 기준 적용: (1) 모든 step이 verified면 Acceptance, (2) flawed가 재평가에서 확정되면 즉시 Rejection, (3) 5회 연속 진행 신호 없이 재개(resumption)되면 Exhaustion으로 전역 halt 및 rejection
• FirstProof challenge, Aletheia가 생성한 정답 증명, OpenAI 솔루션 등 3개 출처에서 21개의 human-expert로 valid/invalid가 확정된 research-grade 증명을 curate하여 평가

Originality

• global judgment에서 constructive elaboration으로의 검증 패러다임 전환: 오류 검출을 "elaboration 실패"라는 생성적 부산물로 재정의
• (Γi, Σi, Ti) tripartite 구조를 통해 각 step의 정리 출처를 명시적으로 강제함으로써 superficial pattern matching을 완화
• fixed confirmation phase와 halting 기준(Acceptance/Rejection/Exhaustion)을 갖춘 state-driven agentic workflow 제안
• 오류를 logical hallucination과 "pedantic hyper-rigor"(암묵적 도메인 관행에서 비롯된 과도한 엄격함)로 구분하는 새로운 failure taxonomy 제시, 이를 통해 expert benchmark 자체의 암묵적 모호성을 노출

Limitation & Further Study

• 평가 규모가 21개의 curated 증명으로 매우 작아 통계적 일반화 가능성이 제한적이며, ground truth의 절대적 명확성을 위해 표본 크기를 희생함
• FirstProof challenge에 크게 의존하므로 다른 수학 분야나 더 넓은 범위의 research-level 증명에 대한 일반화 여부가 불확실
• "pedantic hyper-rigor"로 분류된 오류가 실제로 암묵적 관행 문제인지, 혹은 프레임워크 자체의 한계인지 구분하는 기준이 다소 주관적일 수 있음
• 5회 halting 기준 등 하이퍼파라미터의 민감도 분석이나 더 큰 규모의 벤치마크에 대한 확장 검증이 후속 연구로 필요함
• Lean과 같은 formal verification과의 결합 가능성 및 실제 agentic reasoning 파이프라인 내 통합에 대한 심층 연구가 요구됨

Evaluation

총평: Global evaluation의 context poisoning 문제를 step-level elaboration과 source control로 해결하려는 시도는 개념적으로 신선하고 실용적 함의가 크지만, 21개 샘플이라는 매우 작은 규모의 diagnostic suite에 기반한 proof-of-concept 수준이라 향후 대규모 검증이 필요하다.