최근 인공지능(AI) 기술의 발전으로 수학적 증명을 자동화하고 검증하는 새로운 시대가 도래했습니다. 린(Lean)과 같은 증명 보조 도구(proof assistants)는 수학적 증명을 공리(axioms) 수준까지 확인하며, AI 에이전트(AI agents)는 이러한 증명 작성 과정을 훨씬 저렴하고 효율적으로 만들고 있습니다. 이러한 흐름 속에서 연구진은 고전적인 선형 정칙화 이론(linear regularization theory)과 그 기반이 되는 함수 해석학(functional analysis)을 AI 에이전트가 자동 형식화(autoformalized)한 린 라이브러리 'AutoIP'를 공개했습니다.
AutoIP는 역문제(inverse problems) 분야의 이론을 기계가 검증할 수 있도록 설계된 라이브러리입니다. 기계가 검증한 증명은 오직 형식화된 진술(formal statement)만을 보증하기 때문에, 인간의 역할은 이 형식화된 진술이 원래 의도했던 바를 정확히 표현하는지 확인하는 것입니다. 연구진은 이 라이브러리를 이러한 검토 작업에 최적화하여, 검토자가 형식화된 진술과 자연어 진술을 비교하고 증명 자체를 읽을 필요가 없도록 구성했습니다. 이들의 경험에 따르면, 오류의 위험은 증명보다는 진술 자체에 있으며, 간단한 자동화된 테스트만으로도 기존 문헌의 문제점을 발견할 수 있음을 확인했습니다. 실제로 한 교과서의 정리(theorem)가 주장된 것보다 더 제한적인 가설(hypothesis)을 가지고 있음을 AutoIP를 통해 밝혀내기도 했습니다.
이러한 AI 기반의 수학 증명 자동화 및 검증은 수학 연구 방식에 혁명적인 변화를 가져올 잠재력을 가지고 있습니다. 복잡한 이론의 정합성을 기계적으로 확인하고, 기존 연구의 미묘한 오류를 찾아내는 것은 학문적 정확성을 크게 향상시킬 수 있습니다. 또한, 수학 교육에서도 학생들이 개념의 엄밀한 정의와 증명을 더 쉽게 이해하고 검증할 수 있도록 돕는 도구로 활용될 수 있습니다. 연구진은 역문제 커뮤니티에 AutoIP 라이브러리를 확장하고 활용할 것을 제안하며, 이는 앞으로 다양한 수학 분야에서 AI 기반의 형식화된 증명 시스템이 확산되는 계기가 될 것으로 보입니다.