인공지능(AI) 시스템이 수학적 증명(proof formalization) 분야에서 놀라운 성과를 보이고 있지만, AI가 생성한 증명을 인간이 이해하고 활용하기 위해서는 AI의 사고방식을 더 깊이 이해해야 한다는 연구 결과가 나왔습니다. Bálint Gyevnár와 Simon DeDeo 연구팀은 '시뮬레이션 협업(simulated collaboration)'이라는 새로운 방법론을 통해 AI 에이전트가 증명 과정에서 인간과 어떤 선호도 차이를 보이는지 체계적으로 분석했습니다.
연구팀은 수학 증명 보조 도구인 Lean에서 이루어진 9개의 주요 인간 협업 프로젝트 데이터를 분석했습니다. 이 데이터는 470만 개 이상의 정의와 6천 개 이상의 커밋(commit)을 포함하는 방대한 양입니다. 분석 결과, AI 에이전트는 증명 구성 과정에서 세 가지 주요 특징을 보였습니다. 첫째, AI는 인간보다 명시적으로 표시된 빈칸(explicitly marked gaps)에 훨씬 더 강하게 이끌렸습니다. 둘째, AI는 밀집하게 연결된 증명 중심부(densely connected proof centers)나 복잡하거나 예상치 못한 증명 목표(complex or surprising proof goals)를 상대적으로 회피하는 경향을 보였습니다. 셋째, AI는 예상치 못한 증명 본문(surprising proof bodies)에 상대적으로 강하게 끌리며, 이를 일반적인 형태로 정규화(regularize)하려는 경향이 있었습니다.
이러한 연구 결과는 수학 분야에서 인간과 AI의 효과적인 협업을 위한 중요한 시사점을 제공합니다. AI는 인간이 간과하기 쉬운 명시적 문제 해결에 강점을 보이지만, 전체적인 맥락 이해나 복잡한 문제의 핵심을 파악하는 데는 아직 한계가 있음을 보여줍니다. 따라서 향후 인간-AI 협업 시스템을 설계할 때는 AI의 이러한 맹점(blind spots)을 보완하고, 인간의 직관과 AI의 계산 능력을 최적화하여 상호 보완적인 역할을 수행하도록 유도하는 방안이 필요할 것입니다. 이는 단순히 AI가 증명을 '생성'하는 것을 넘어, 인간이 증명을 '이해'하고 '활용'하는 데 도움을 주는 방향으로 AI 기술이 발전해야 함을 의미합니다.