OpenAI가 유체역학 분야의 오랜 난제인 나비에-스토크스(Navier-Stokes) 방정식에 대한 증명을 발표하며, 이와 함께 기계로 검증할 수 있는 '린 4(Lean 4)' 형식 증명을 공개했습니다. 최근 AI가 해결한 다른 수학적 추측들에서도 형식 증명이 함께 제공되었으며, 특히 린 4가 주로 사용되고 있습니다. 이는 AI가 복잡한 수학적 문제를 해결하는 과정에서 그 결과의 신뢰성을 확보하기 위한 핵심적인 방법론으로 형식 증명이 부상하고 있음을 보여줍니다.
과거 형식 증명(formal proof)을 생성하는 작업은 극도로 많은 시간과 노력이 필요했습니다. 2005년 추정치에 따르면, 학부 수학 교과서 한 페이지를 형식화하는 데 약 40시간이 소요되었고, 연구 논문은 내용의 밀도와 광범위한 선행 연구 의존성 때문에 교과서보다 20배 이상 어렵다고 평가되었습니다. 이러한 기준으로 OpenAI의 166쪽 논문을 형식화하려면 약 132,800인시(人時)가 필요할 것으로 계산됩니다. 하지만 OpenAI가 린 4를 통해 이 증명을 검증하는 데 걸린 시간은 단 17시간이었습니다. 이는 형식화 작업량 추정치와 검증 시간을 직접 비교할 수는 없지만, AI의 도움으로 형식 증명 과정의 효율성이 혁신적으로 개선될 수 있음을 시사하는 대목입니다.
이러한 형식 검증 기술은 단순히 수학 연구에만 국한되지 않고 다양한 실용 분야에 적용될 수 있습니다. 예를 들어, 보안 정책 집합의 일관성을 검증하거나, 스마트 계약(smart contract)이 특정 최대 책임 한도를 준수하는지 확인하고, 임무 수행에 필수적인 알고리듬(algorithm)의 정확성을 검증하는 데 활용될 수 있습니다. 이러한 실무적 문제들은 수학 연구의 형식화보다 검증이 더 쉽고, 투자 대비 수익(ROI)을 정량화하기도 용이하다는 장점이 있습니다. AI와 형식 증명의 결합은 복잡한 시스템의 신뢰성과 안정성을 확보하는 데 중요한 역할을 할 것으로 기대됩니다.