엄격한 단계별 검증을 통한 연구 수준의 수학 증명 평가

대규모 언어 모델 (LLMs)은 복잡한 수학적 증명을 엄격하게 검증하는 데 어려움을 겪습니다. 표준적인 전역 평가 (Global evaluation) 방식은 표면적으로 그럴듯한 진술이 미묘한 논리적 결함을 가려, 환각 (Hallucination) 또는 과도한 회의론으로 이어지는 "문맥 오염 (Context poisoning)" 문제를 겪습니다. 이를 해결하기 위해, 우리는 전역 평가에서 엄격한 단계별 검증 (Step-level verification)으로 전환합니다. 우리의 프레임워크는 각 추론 단계에 대한 상세한 문맥을 유지하며, 적용된 정리 (Theorems)의 출처를 엄격하게 제한합니다. 우리는 FirstProof 챌린지에서 추출한 연구 수준의 증명들로 구성된 정교하게 큐레이션된 적대적 진단 스위트 (Adversarial diagnostic suite)를 통해 평가를 수행합니다. 체계적인 어블레이션 연구 (Ablation study)는 이러한 연역적 제약 (Deductive constraints)이 필수적임을 보여주며, 제약이 없는 전역 프롬프팅 (Global prompting)은 미묘한 논리적 오류를 국지화하는 데 지속적으로 실패합니다. 전역 평가보다 우수한 성능을 보이는 것을 넘어, 우리의 접근 방식은 실패 분류 체계 (Failure taxonomy)를 근본적으로 변화시킵니다. 오류 분석 결과, 심각한 논리적 환각을 보이는 대신, 남은 거절 사례들은 주로 명시되지 않은 도메인 관례에서 비롯된 "지나치게 까다로운 엄격함 (Pedantic hyper-rigor)"의 사례들이었으며, 이는 전문가 벤치마크 자체 내에 존재하는 암묵적인 모호성을 효과적으로 드러냅니다. 우리의 연구 결과는 에이전트 (Agents)가 검증 노트를 신중하고 인간 수학자와 유사한 방식으로 정리하도록 프롬프팅하는 것이, 엄격한 증명과 결함이 있는 증명을 구별하는 능력을 실질적으로 향상시킬 수 있음을 시사합니다. 이는 베이스 모델 (Base model)이 아직 잘 알지 못하는 최첨단 수학 개념에 대한 에이전트 추론 (Agentic reasoning)을 강화하고, 향후 자동화된 증명 검토 시스템을 위한 이론적 토대를 마련할 잠재력을 가집니다. 코드와 프롬프트는 GitHub에서 확인할 수 있습니다.