기술 요약: 컴퓨터 과학을 위한 논리의 이론 규모 자동 형식화 (Theory-Scale Auto-Formalization)

문제 정의

자동 형식화(Auto-formalization)—비형식적 수학 및 논리를 기계 검증 가능한 문장과 증명으로 번역하는 것—는 확장 가능한 형식 검증을 향한 중요한 단계이다. 그러나 기존의 진전은 주로 고립된 문장이나 작고 자기 완결적인 문제들에 국한되어 있다. 수백 개의 상호 의존적인 정의, 보조정리, 정리를 하나의 통일된 형식 체계로 일관되게 번역해야 하는 **이론 규모 자동 형식화(Theory-scale auto-formalization)**는 여전히 해결되지 않은 과제로 남아 있다.

현재의 벤치마크들은 다음과 같은 이유로 이 설정을 적절히 다루지 못한다:

1. 이질적인 아티팩트(정의, 알고리즘, 증명)를 포함한 전체 전개 과정보다는 고립된 문장에 집중한다.
2. 성숙하고 기존에 존재하는 라이브러리(예: Mathlib)에 과도하게 의존하여, 기초부터 이론을 구축하는 데 따르는 난이도를 가린다.
3. 대규모의 상호 연결된 코드베이스 전반에 걸쳐 충실도(faithfulness)와 일관성을 평가할 수 있는 맞춤형 평가 프로토콜이 부족하다.

이 설정에서의 핵심 과제는 전역적 일관성을 유지하고, 소스 텍스트(특히 암시적 가정 및 그래픽 정의)에 대한 충실도를 보존하며, 구문적으로 유효할 뿐만 아니라 형식적으로 증명 가능한 아티팩트를 생성하는 것이다.

방법론

LCS-Bench 벤치마크

저자들은 교과서 Logics for Computer Science: Foundations of Automatic Theorem Proving (제2판)에서 파생된 독립적인 이론 규모 벤치마크인 LCS-Bench를 소개한다. 이전의 벤치마크들과 달리, LCS-Bench는 Mathlib와 같은 외부 라이브러리에 의존하지 않으며, 하나의 일관된 전개 내에서 광범위한 형식화 작업을 다룬다.

아티팩트의 범위:

• 소스: 명제 논리, 1차 논리, 정리 증명, 그리고 논리 프로그래밍(Prolog 포함)을 다루는 8개의 장(chapter).
• 내용: 4,076개의 **Lean 선언(declarations)**과 85,000라인 이상의 Lean 코드(28,000라인의 증명 포함)로 형식화된 327개의 교과서 항목.
• 이질성: 이 벤치마크는 단순한 정리가 아니라 도메인 특화 언어(DSL), 깊게 임베딩된 증명 트리, 알고리즘, 그리고 메타 이론을 포함한다.

반자동 에이전트 파이프라인

이 벤치마크는 Claude Opus 4.6 및 GPT-5.3과 같은 대규모 언어 모델(LLM)을 활용한 에이전트 루프와 인간 전문가의 검토를 결합한 새로운 4단계 반자동 파이프라인을 사용하여 구축되었다:

1. 전처리(Pre-processing): 교과서 PDF를 구조화된 Markdown으로 변환하고, 그래픽(추론 규칙, 증명 트리)을 ASCII 다이어그램으로 수동으로 다시 그리며, 산문으로 표현된 암시적 형식 문장(예: 스코프 제한)에 주석을 단다.
2. 형식화 계획(Formalization Planning): 에이전트가 두 층의 중간 표현(IR)을 생성한다:
   • 키워드와 하위 절(sub-clause)을 교과서 수준의 관계(IS-A, RELIES-ON)로 매핑하는 개념 그래프(Concept Graph).
   • 개념을 Lean 구현체로 매핑하여 "임베딩 레벨"(구문적 DSL을 위한 deep, 의미론적 속성을 위한 shallow, 메타 정리의 경우 mixed)을 결정하는 형식 시그니처 그래프(Formal Signature Graph).
3. Lean 구현(Lean Implementation): 에이전트 구현체가 의존성을 준수하는 세 단계의 라운드를 통해 모듈을 Lean 코드로 번역한다:
   • 라운드 1: 구조(Structures) 및 귀납적 타입(Inductive types).
   • 라운드 2: 정의, 함수 및 예시.
   • 라운드 3: 정리 및 보조정리 문장 ( sorry 플레이스홀더 포함).
4. 형식적 정확성 검토(Formal Correctness Review): 파이프라인은 반례 탐색(부정을 증명하려고 시도함)과 이슈 트래킹을 사용하여 sorry 플레이스홀더를 채운다. 결정적으로, 인간 전문가가 불충실성, 누락된 가정, 그리고 에이전트가 잘못된 정의 위에 워크아웃을 축적하는 "잘못된 토대(false foundations)" 문제를 해결하기 위해 개입한다. 전문가들은 약 6인월(person-months)을 투자하여 주요 정의와 핵심 정리의 약 30%를 재작성했다.

평가 프로토콜

LCS-Bench는 데이터 엔진을 통해 도출된 5가지 평가 트랙을 지원한다:

• 자동 형식화 (AF):
  • IAF (항목 단위): 컨텍스트가 주어진 상태에서 단일 교과서 항목을 형식화한다.
  • SSAF (소절 단위): 소절 내의 모든 항목을 형식화한다.
  • IAF-D: 강건성을 테스트하기 위해 방해 선언(distractor declarations)을 주입한 IAF.
• 정리 증명 (TP):
  • DTP (선언 단위): 단일 sorry가 포함된 선언을 증명한다.
  • ITP (항목 단위): 모든 sorry가 채워진 전체 교과서 정리/보조정리를 증명한다.

새로운 지표: 저자들은 논리적 동등성을 넘어 정의적 동등성을 검사하는 정의 방정식 체커인 DefEq Checker를 도입한다. 이는 타입 정의, 귀납적 타입, 생성자를 검증하기 위해 정의적 동등성(ISDEFEQ) 또는 congruence closure(GRIND)를 체크함으로써, 데이터셋에 존재하는 이질적인 선언 종류들을 처리한다.

주요 결과

저자들은 14개의 모델(Claude Opus 4.6 및 GPT-5.4와 같은 독점 모델과 DeepSeek, Kimi, Qwen과 같은 오픈 소스 모델 포함)을 제로샷, 사고(thinking), 에이전트 모드에 걸쳐 평가했다.

1. 높은 난이도: 이 벤치마크는 매우 도전적이다. 최첨단 모델인 Claude Opus 4.6(에이전트 모드)은 항목 단위 자동 형식화(IAF) 트랙에서 단 20.1%의 통과율을 기록했다.
2. 품질 및 일관성: 벤치마크 아티팩트는 엄격한 인간 참여형 검토와 DefEq Checker를 통해 검증되었으며, 품질이 높고 일관되며 소스 텍스트에 충실하다.
3. 성능 추세:
   • 컨텍스트 민감도: 컨텍스트가 확장됨에 따라 성능이 급격히 저하된다 (SSAF 통과율은 한 자릿수에 불과하다). 방해 요소(IAF-D)를 추가하면 성능이 일관되게 저하되는데, 이는 모델이 긴 컨텍스트에서 중요한 정보를 식별하는 데 어려움을 겪음을 나타낸다.
   • 항목 유형: 모델은 정의 및 의미론적 주장(모델, 진리)에 대해서는 가장 높은 성능을 보이지만, 구문적 인프라(도출, 공식) 및 알고리즘적 내용에 대해서는 크게 고전한다.
   • 컴퓨팅 vs 역량: 테스트 시간 컴퓨팅(사고 또는 에이전트 루프를 통한)을 늘리는 것은 완만한 이득을 제공하지만 근본적인 어려움을 해결하지는 못한다. 잘못된 출력은 종종 솔루션으로 수렴하기보다는 "과잉 사고(overthinking)"(더 많은 토큰/턴 발생)하는 양상을 보인다.
   • 오류 분석: 지배적인 실패 모드는 NMExpr(non-matching expression)로, 생성된 코드가 컴파일은 되지만 의미적으로는 틀린 경우이다. 강력한 모델들 사이에서는 컴파일 실패가 덜 흔하게 나타난다.

의의 및 주장

이 논문은 초점을 고립된 문장 번역에서 이론 규모의 전개로 전환함으로써, 형식 방법론을 위한 AI 역량을 평가하는 데 있어 LCS-Bench가 중요한 진전임을 주장한다.

• 벤치마킹의 현실: 이는 현재의 LLM이 이론 규모의 자동 형식화를 해결하기에는 아직 멀었음을 보여주며, 논리적 인프라의 복잡성이 증가함에 따라 성능이 저하됨을 드러낸다.
• 방법론적 통찰: 연구는 주요 병목 현상이 단순히 논리적 추론뿐만 아니라, 반형식적 수학 영어(도형, 생략 부호, 암시적 가정)를 정밀한 기호 표현으로 번역하는 것, 특히 바인더(binder) 및 치환(substitution)과 같은 구문적 인프라를 다루는 것임을 강조한다.
• 향atic 방향: 저자들은 발전 방향이 단순히 테스트 시간 컴퓨팅을 확장하는 것이 아니라, 바인더/치환 추론 및 상호/귀납적 타입 정의를 다루는 더 깊은 내재적 능력(innate capabilities)을 요구한다고 제안한다. 이 벤치마크는 신경 기호적(neurosymbolic) 및 에이전트 기반의 형식 검증을 개발하기 위한 엄격하고 독립적인 테스트베드 역할을 한다.

이 작업은 이론 규모의 자동 형식을 AI가 패턴 매칭을 넘어서서, 처음부터 일관되고 검증 가능한 수학적 이론을 구축해야 하는 핵심적인 최전선으로 위치시킨다.