MathCoPilot: 인간-AI 공생 패러다임을 위한 인터랙티브 시스템 - 수학 연구

MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research

기존의 LLM 기반 정리 증명 도구는 형식 수학 벤치마크에서 인상적인 결과를 보여주었지만, 여전히 주어진 명제를 자율적으로 증명하는 에이전트 역할을 수행하는 데 한계가 있습니다. 본 논문에서는 MathCoPilot이라는 인간-AI 공생 패러다임을 구현한 시스템을 제안합니다. 이 시스템에서 수학자는 전체적인 방향을 제시하고, AI 에이전트는 지속적인 인간의 지침 하에 세부적인 형식화 및 증명 작업을 수행합니다. MathCoPilot은 다음 세 가지 핵심 기능을 통합합니다: (1) 수학자와 AI 에이전트가 협력하는 인터랙티브 작업 공간으로, 사용자가 직접 검토하고, 지시하며, 개선할 수 있도록 증명을 탐색 가능한 단계로 분해한 '증명 청사진'을 제공합니다. (2) 적응형 지식 베이스 검색 및 Lean 통합 반복 검증 기능을 갖춘 자동 증명 기술 오케스트레이션입니다. (3) 주제 기반 논문 검색 및 검증된 Lean 지식 베이스로의 자동 형식화 기능입니다. MathCoPilot을 사용하여 Gemini~3.1~Pro, GPT-5.4, Claude~Opus~4.7을 포함한 최첨단 LLM 4개를 FormalMATH 데이터셋과 실제 PDE 정리 두 가지에 대해 비교 분석했습니다. 검증된 Lean~4 증명을 생성하고 의도적으로 오류가 포함된 증명에서 오류를 식별하는 능력 등을 평가했습니다. 그 결과, 현재 모델은 유리한 자동 형식화 조건 하에서 학부 수준의 문제를 높은 성공률로 해결할 수 있지만, 진정한 수학적 이해력을 요구하는 특정 분야의 정리에는 여전히 상당한 어려움이 존재한다는 것을 확인했습니다.

Existing LLM-based theorem provers have achieved impressive results on formal mathematics benchmarks, yet they remain confined to acting as autonomous agents that prove a stated proposition. In this paper, we propose MathCoPilot, a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research, in which the mathematician steers the high-level mathematical direction while AI agents carry out the detailed formalization and proof work under continuous human guidance. MathCoPilot unifies three core capabilities: (1) an interactive workbench where the mathematician and AI agents collaborate through a living proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; (2) automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and (3) topic-driven paper retrieval and automated formalization into a verified Lean knowledge base. Using MathCoPilot, we systematically compare four state-of-the-art LLMs, including Gemini~3.1~Pro, GPT-5.4, and Claude~Opus~4.7, on a FormalMATH subset and on two real PDE theorems requiring deep domain expertise, evaluating their ability to produce verified Lean~4 proofs and to identify errors in deliberately incorrect proofs. Our results show that while current models can handle undergraduate-level problems with high success rates under favorable autoformalization conditions, substantial challenges remain for domain-specific theorems requiring genuine mathematical understanding.