컴퓨터 과학 논리를 위한 이론 규모의 자동 형식화 (Theory-Scale Auto-Formalization)

자동 형식화 (Auto-formalization)는 확장 가능한 형식 검증 (formal verification)을 위해 매우 중요하지만, 기존의 진전은 주로 고립된 문장들에 집중되어 있습니다. 반면, 수백 개의 상호 의존적인 정의 (definitions), 보조정리 (lemmas), 그리고 정리 (theorems)를 일관되게 번역하는 이론 규모의 자동 형식화 (theory-scale auto-formalization)는 일관성 (consistency), 충실성 (faithfulness), 확장성 (scalability), 그리고 정확성 (correctness)의 문제로 인해 여전히 미해결 과제로 남아 있습니다. 본 논문에서는 컴퓨터 과학 논리 (Logics for Computer Science)를 기반으로 한 독립적인 이론 규모 벤치마크인 LCS-Bench를 소개합니다. LCS-Bench는 개념 그래프 (concept graphs), 형식 시그니처 계획 (formal signature planning), 이슈 트래킹 (issue tracking), 반례 탐색을 통한 sorry-filling (sorry-filling with counter-example search)을 활용하고, 인간 전문가의 충실성 검토 (faithfulness review)를 통해 보완되는 새로운 반자동 에이전트 파이프라인 (semi-automated agentic pipeline)을 통해 구축되었습니다. 그 결과물은 327개의 교과서 항목, 4,076개 이상의 Lean 선언 (declarations), 그리고 85,000라인 이상의 Lean 코드를 포함합니다. 이 데이터셋은 자동 형식화 및 정리 증명 (theorem-proving) 능력의 다양한 측면을 측정하는 5가지 트랙의 평가 벤치마크를 자동으로 도출하는 데이터 엔진을 통해 광범위한 평가를 지원합니다. 또한, 우리는 정의적 동등성 검사기 (definitional equivalence checkers)를 특징으로 하는 새로운 평가 프로토콜을 도입하여, 더욱 세밀하고 충실한 평가를 가능하게 합니다. 14개의 모델에 대한 광범위한 평가를 통해 우리는 다음을 입증합니다: (1) LCS-Bench는 고품질이며 일관되고 충실합니다; (2) 이 벤치마크는 도전적이며, 최신 모델(state-of-the-art models)조차 자동 형식화 작업에서 20.1%의 성적만을 달성했습니다; (3) 우리의 분석은 이론 규모의 자동 형식화에 관한 주요 발견을 드러내며 향후 연구를 위한 유망한 방향을 제시합니다.