완화된 자연 형식 언어(Relaxed Natural Formal Language)를 이용한 수학의 검증 가능한 자동 형식화

자동 형식화 (Auto-formalization)는 비형식적인 수학적 내용을 정리 증명기 (theorem provers)가 처리할 수 있는 형식 언어 (formal languages)로 번역하는 것을 목표로 합니다. 그러나 기존의 정리 증명기를 직접 대상으로 하는 것은 LLM이 비형식적인 수학적 서술과 형식 증명 언어 사이의 상당한 표현적 격차 (representational gap)를 메워야 함을 의미합니다. 이러한 격차는 의미론적 일관성 (semantic consistency)을 평가하는 것도 어렵게 만듭니다. 우리는 자동 형식화를 위한 중간 목표로서 완화된 자연 형식 언어 (Relaxed Natural Formal Language, Relaxed NFL)를 도입하여 이러한 어려움을 해결합니다. Relaxed NFL은 비형식적인 수학적 서술과 가깝게 유지되도록 설계되었습니다. 즉, 비형식적 추론의 일반적인 구조를 보존하며, 자동 형식화 단계에서 그 정확한 해석이 고정될 필요 없이 부분적으로 지정된 표현식과 명제를 허용합니다. 비형식적 추론에서 상속된 나머지 모호성과 암시성은 이후의 정교화 (elaboration) 단계에서 해결되며, 이 단계는 Relaxed NFL 증명을 형식적으로 정의된 의미론을 가진 핵심 자연 형식 언어 (Core Natural Formal Language, Core NFL) 증명으로 변환합니다. 정교화 절차는 규칙 기반 변환 (rule-based transformations)과 LLM이 생성한 휴리스틱 (heuristics)을 결합하는 동시에, 각 변환 단계에 대한 명시적인 제약을 통해 검증 가능성 (verifiability)을 유지합니다. 그런 다음 Core NFL은 증명 간극 (proof gaps), 즉 형식화된 증명이 정확하기 위해 반드시 성립해야 하는 검증 조건 (verification conditions)을 생성하는 데 사용됩니다. 이러한 간극은 도메인 특화 전술 언어 (domain-specific tactic language)로 작성된 LLM 생성 증명 스크립트에 의해 해소되며, 이 언어는 우리 시스템의 일부로 구현된 정리 라이브러리 (theorem libraries) 및 도메인 특화 솔버 (domain-specific solvers)를 호출하기 위한 명령어를 제공합니다.