인간 + AI + 증명 보조기, 세 힘을 합쳐 크누스의 난제에 도전하다

크누스가 던진 수학 문제, AI와 함께 풀다

컴퓨터 과학의 아버지라 불리는 도널드 크누스(Donald Knuth) 교수를 아시나요? "The Art of Computer Programming"이라는 전설적인 책을 쓴 분인데요. 크누스 교수가 제시한 조합론 문제 중 하나인 "Claude Cycles" 문제에 대해 인간 수학자, AI(대규모 언어 모델), 그리고 형식 증명 보조기(proof assistant)가 협력해서 새로운 진전을 이뤄냈다는 소식이에요.

Bo Wang이라는 연구자가 이 협업 과정과 결과를 공유했는데, 세 가지 서로 다른 능력을 가진 도구가 함께 작업하는 방식이 앞으로 수학과 컴퓨터 과학 연구의 패러다임을 바꿀 수 있다는 점에서 주목할 만해요.

증명 보조기가 뭔데?

이게 뭐냐면, 수학 증명을 컴퓨터가 검증해주는 소프트웨어예요. 대표적으로 Lean, Coq, Isabelle 같은 도구가 있는데, 사람이 증명의 각 단계를 코드처럼 작성하면 컴퓨터가 "이 논리 전개가 맞는지" 기계적으로 확인해주는 거예요. 마치 컴파일러가 코드의 문법 오류를 잡아주듯이, 증명 보조기는 논리적 오류를 잡아주는 거죠.

전통적으로 수학 증명은 사람이 쓰고 다른 사람이 검토하는 방식(peer review)으로 검증했는데, 증명이 수백 페이지에 달하면 실수를 놓치기 쉽거든요. 증명 보조기를 쓰면 한 줄 한 줄 기계가 확인해주니까 훨씬 신뢰도가 높아져요.

인간, AI, 증명 보조기의 삼각 협업

이번 연구에서 흥미로운 건 각 참여자의 역할 분담이에요. 인간 수학자는 전체 전략과 직관을 제공하고, AI(LLM)는 가능한 접근법을 빠르게 탐색하고 아이디어를 생성하며, 증명 보조기는 제안된 증명이 논리적으로 완전한지 최종 검증하는 역할을 맡았어요.

이걸 소프트웨어 개발에 비유하면 이해가 쉬운데요. 인간은 시니어 아키텍트처럼 큰 방향을 잡고, AI는 주니어 개발자처럼 코드를 빠르게 작성하며, 증명 보조기는 CI/CD 파이프라인의 테스트 스위트처럼 결과물을 자동으로 검증하는 거예요. AI가 아무리 그럴듯한 증명을 생성해도 증명 보조기를 통과하지 못하면 의미가 없고, 인간의 직관 없이는 AI가 올바른 방향을 찾기 어렵고요.

특히 AI의 역할이 중요한데, LLM은 수학적으로 엄밀하지 않은 결과를 낼 수 있지만(소위 "할루시네이션"), 증명 보조기가 이를 필터링해주기 때문에 AI의 약점이 상쇄돼요. 반대로 AI의 강점인 빠른 탐색 능력 덕분에 인간 혼자서는 시도하기 어려웠던 접근법들을 대량으로 테스트할 수 있게 되는 거죠.

업계 흐름에서 보면

이런 AI + 형식 검증의 결합은 최근 뜨거운 연구 분야예요. 구글 딥마인드의 AlphaProof가 국제 수학 올림피아드 문제를 형식 증명으로 풀어낸 것도 같은 맥락이고, Meta의 Lean 기반 수학 증명 자동화 연구, OpenAI의 형식 추론 연구 등이 모두 이 방향을 향하고 있어요.

기존에는 "AI가 수학 증명을 대신해줄 수 있을까?"라는 질문이었다면, 이제는 "인간과 AI와 형식 도구가 어떻게 최적으로 협력할 수 있을까?"로 질문이 바뀌고 있는 거예요. 이건 수학뿐 아니라 소프트웨어 검증, 하드웨어 설계 검증, 심지어 법률 논증 같은 영역에도 영향을 줄 수 있는 패러다임 변화예요.

개발자에게 주는 시사점

소프트웨어 개발에서도 비슷한 패턴이 적용돼요. AI 코딩 어시스턴트가 코드를 생성하고, 타입 시스템이나 정적 분석 도구, 테스트가 이를 검증하는 구조는 이미 우리가 일상적으로 쓰고 있잖아요. "AI가 생성하고 형식 시스템이 검증한다"는 이 삼각 구도는 앞으로 점점 더 보편화될 거예요.

Lean이나 Coq 같은 증명 보조기에 관심 있다면 지금 배워두면 좋아요. 특히 Lean 4는 범용 프로그래밍 언어로도 쓸 수 있어서 진입장벽이 예전보다 많이 낮아졌거든요. 당장 실무에 쓰지 않더라도 형식적 사고방식을 익히는 것 자체가 코드 품질을 높이는 데 도움이 돼요.