개별 정리 번역을 넘어 이론 전체를 형식화하는 AI

들어가며

자동 형식화는 자연어로 쓰인 수학적·과학적 내용을 기계가 검증할 수 있는 형식 언어로 옮기는 기술이다. 지금까지 많은 연구는 비교적 분명한 과제에 집중했다. 비형식적인 하나의 명제를 Lean, Coq, Isabelle 같은 형식 시스템이 검사할 수 있는 문장으로 변환하는 것이다.

하지만 arXiv 논문 “Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases”는 이러한 접근만으로는 실제 형식화의 본질을 포착하기 어렵다고 본다. 현실의 정리는 홀로 존재하지 않는다. 정의, 공리, 보조정리, 표기법, 기존 결과와 연결된 넓은 맥락 속에서만 제대로 표현될 수 있다.

핵심 내용

• 형식화는 단순 번역이 아니다. 하나의 정리를 정확히 기술하려면 그 정리를 가능하게 하는 개념, 전제, 중간 결과가 먼저 마련되어야 한다.
• 진짜 산출물은 구조화된 라이브러리다. 검증된 단일 문장은 활용 가치가 제한적이다. 반면 일관된 형식 라이브러리는 이후 증명, 검증 도구, 교육, 자동 추론 시스템에서 반복적으로 재사용될 수 있다.
• 문제 정의가 확장된다. 이론 수준 자동 형식화는 이름 짓기, 모듈 구성, 의존 그래프, 개념 일관성, 기존 라이브러리와의 연결을 다뤄야 한다.
• 평가 방식도 달라져야 한다. 특정 문장이 타입 검사를 통과하는지만으로는 생성된 이론이 잘 구조화되었는지, 유지보수 가능한지, 충분히 포괄적인지 판단하기 어렵다.
• 논문은 연구 의제를 제시한다. 저자들은 이 전환의 중요성, 대안적 관점, 열린 문제, 앞으로의 유망한 경로를 정리한다.

의미와 영향

이 주장은 자동 형식화를 ‘언어 변환’에서 ‘지식 공학’으로 확장한다. AI for Science 관점에서 보면, 미래의 시스템이 교과서, 논문, 분야별 문서를 검증 가능한 형식 라이브러리로 바꿀 수 있다면 수학 지식 정리, 과학 이론 검증, 고신뢰 소프트웨어 개발에 기여할 수 있다.

또한 이 논문은 현재 AI 시스템의 한계를 드러낸다. 형식화에서 중요한 것은 문법적으로 맞는 코드를 생성하는 능력만이 아니다. 긴 맥락을 유지하고, 추상화 수준을 조절하며, 의존관계를 추적하고, 기존 라이브러리와 조화시키는 능력이 필요하다. 이는 일회성 번역보다 인간 전문가의 실제 작업 방식에 훨씬 가깝다.

물론 저자들이 이 문제가 이미 해결됐다고 주장하는 것은 아니다. 이 논문은 자동 형식화 연구가 더 현실적이고 재사용 가능한 목표를 향해야 한다는 제안에 가깝다. 이론 수준 자동 형식화가 성숙한다면, 통합적이고 검증 가능한 형식 지식베이스 구축의 기반이 될 수 있다.

출처: arXiv