기술 요약: 컴파일을 넘어: 충실한 자연어-Lean 문장 정식화 평가

1. 문제 정의

본 논문은 자연어-Lean 문장 정식화(natural-language-to-Lean statement formalization) 과제를 다룹니다. 이는 비형식적인 수학적 문장을 유효한 Lean 4 정리 선언(theorem declaration)으로 자동 변환하는 작업입니다. 이 과제는 정리 증명(theorem proving)과는 구별됩니다. 정리 증명 벤치마크(예: MiniF2F, LeanDojo)에서는 정식 문장이 고정되어 있고 신뢰할 수 있는 상태이며, 시스템의 목표는 검증기에 의해 수용되는 증명을 생성하는 것입니다. 반면, 문장 정식화에서는 시스템이 문장 자체를 생성해야 합니다.

핵심적인 도전 과제는 컴파일이 성공을 위한 필요조건이지만 충분조건은 아니라는 점입니다. Lean 선언은 다음과 같은 상황에서도 컴파일(타입 체크)될 수 있습니다:

• 중요한 가설을 누락함.
• 논의의 영역(domain of discourse)을 변경함.
• 주장을 강화하거나 약화시킴.
• 결과의 공허한(vacuous) 버전을 인코딩함.

기존 연구들은 종종 컴파일 성공률이나 참조 기반 등가성 메트릭(예: BEq, 역번역)에 의존해 왔습니다. 본 논문은 컴파일만으로는 시스템이 성공한 것처럼 보이지만 실제로는 의도된 수학적 의미를 보존하지 못하는 "컴파일 통과 격차(compile-pass gap)"를 발생시킨다고 주장합니다. 저자들은 핵심 문제를 충실한 문장 정식화(faithful statement formalization), 즉 컴파일되면서 동시에 원래의 자연어 입력의 의미적 의도를 보존하는 선언을 생성하는 것으로 정의합니다.

2. 방법론

2.1 벤치마크 구축

저자들은 오픈 소스 LaTeX 강의 노트와 교과서에서 추출한 400개의 자연어 문장으로 구성된 대학원 수준의 벤치마크를 큐레이션했습니다. 이 데이터셋은 네 가지 영역에 걸쳐 균형 있게 구성되었습니다:

• 실해석학 (Real Analysis) (100개 항목)
• 복소해석학 (Complex Analysis) (100개 항목)
• 위상수학 (Topology) (100개 항목)
• 대수학 (Algebra) (100개 항목)

결정적으로, 이 문장들은 동반되는 골드(gold) Lean 선언이 없으며, 이는 이 과제가 단순한 검색이 아닌 진정한 번역 과정을 나타내도록 보장합니다.

2.2 평가 프로토콜

논문은 충실성을 평가하기 위해 인간 전문가에 의해 보정된 합의 기반 LLM-as-Judge(Consensus LLM-as-Judge) 메트릭을 제안합니다. 프로토콜은 두 단계로 구성됩니다:

1. 컴파일러 검증: 컴파일에 실패한 코드는 즉시 불충실한 것으로 간주됩니다.
2. 의미적 합의: 컴파일되는 코드의 경우, 두 개의 독립적인 LLM 심사역(GPT-5.2 및 Gemini-2.5-Pro)이 생성된 Lean 선언을 원래의 자연어 문장과 비교합니다. 이들은 충실도 점수(0–10)를 부여합니다.
   • 성공 지표: 번역이 **충실하다(Faithful)**고 간주되려면 반드시 컴파일되어야 하며 동시에 두 심사역 모두 점수를 9점 이상으로 부여해야 합니다.
   • 이 엄격한 합의 접근 방식은 시스템 비교를 위한 공식적인 동등성 증명이 아니라, 보수적인 운영 지점으로 설계되었습니다.

2.3 인간 보정

자동화된 메트릭을 검증하기 위해 저자들은 인간 감사를 실시했습니다:

• 합의 긍정(Consensus-Positive): 엄격한 합의를 통해 충실하다고 레이블링된 출력 중 96.0%가 인간 검토자에 의해 충서한 것으로 확인되었습니다.
• 합의 부정(Consensus-Negative, 컴파일 통과): 컴파일되었으나 합의에서 거부된 출력 중 82.4%가 인간에 의해 실제 의미적 실패로 확인되었습니다.
  이는 해당 메트릭이 의미적 표류(semantic drift)를 효과적으로 식별하는 고정밀도의 보수적인 필터임을 입증합니다.

2.4 실험 설정: 요인 설계(Factorial Design)

저자들은 세 가지 일반적인 개입의 효과를 분해하기 위해 $2^3$ 요인 설계를 사용하여 다양한 시스템(범용 LLM, 특화된 정식화 모델, 증명 지향 모델, 도구 증강 에이전트)을 평가했습니다:

1. 매개변수적 전문가 초안 작성 (T): 미세 조정된 모델(Herald)을 사용하여 초기 초안을 생성합니다.
2. 지식 검색 (S): Mathlib을 쿼리(심볼 조회, 네임스페이스 해결)하고 근거를 찾기 위해 웹 검색을 수행하는 도구를 사용합니다.
3. Lean 정교화 피드백 (F): REPL을 사용하여 코드를 반복적으로 컴파일하고 수정을 위한 에러 메시지를 받습니다.

에이전트 아키텍처는 상태를 유지하고 구성에 따라 어떤 도구를 호출할지 결정하는 중앙 오케스트레이터(GPT-5.2)를 사용합니다.

3. 주요 결과

3.1 컴파일 통과 격차 (The Compile-Pass Gap)

가장 중요한 실증적 발견은 컴파일 성공률과 의미적 충실성 사이의 괴리입니다:

• 전체 도구 증강 에이전트는 89.5%의 컴파일 성공률을 달랐습니다.
• 그러나 엄격한 합의 메트릭 하에서, 단 **60.5%**만이 충실한 것으로 간주되었습니다.
• 이는 출력이 컴파일되지만 의미 검사를 통과하지 못하는 29.0포인트의 격차를 남깁니다. 인간 감사는 "컴파일 통과, 합의 부정" 사례의 대다수가 실제 의미적 실패(예: 가설 누락, 공허한 주장)임을 확인했습니다.

3.2 모델 성능

• 특화된 정식화 모델 및 증명 모델: 전용 정식화 모델(예: Herald, Kimina-Autoformalizer)과 증명 지향 모델(예: Goedel-Prover, Kimina-Prover)은 공식 타겟이 제공되지 않은 상태에서 문장 생성 시 낮은 성능을 보였습니다. 이들의 충실도 비율은 4.0%에서 12.3% 사이였습니다.
• 일반 LLM: 원샷(one-shot) 범용 LLM은 19.8~28.0%의 충실도를 기록했습니다.
• 도구 증강 에이전트: 전체 에이전트 프레임워크는 원샷 베이스라인을 크게 상회하여 60.5%의 충실도에 도달했습니다. 그러나 서로 다른 오케스트레이터(Sonnet 4.5, Gemini-2.5-Pro)는 베이스라인이 다름에도 불구하고 유사한 성능 수준(60~65%)으로 수렴했는데, 이는 이득이 특정 오케스트레이터 모델보다는 도구 증강 접근 방식의 구조적 특징임을 시사합니다.

3.3 개입의 요인 분해

연구는 세 가지 도구의 영향을 격리하여 분석했습니다:

• 정교화 피드백 (F): 유효성(validity)(컴파일)의 가장 큰 동력이었습니다. 이는 컴파일 성공률을 크게 높였지만, 동시에 문법적으로는 맞지만 의미적으로 표류한 문장들도 통과하게 함으로써 "컴파일 통과하지만 불충실한" 범주를 확장시키기도 했습니다.
• 검색 (S): 검색은 주로 **근거 형성(grounding)과 선택성(selectivity)**을 개선했습니다. 이는 컴파일 통과 격차를 줄였으며(즉, 컴파일은 되지만 의미적으로 틀린 문장을 걸러내는 데 도움을 줌), 피드백이 없을 때 가장 높은 한계 효용을 보였습니다.
• 전문가 초안 작성 (T): 미세 조정된 초안 사전 지식은 피드백과 근거가 확보되면 대체 가능한 수준이었습니다. 실제로 완전한 피드백이 있는 경우, 초안 사전 지식은 오히려 성능을 약간 저하시켰는데, 이는 강력한 오케스트레이터가 컴파일러 피드백을 받을 때 특화된 초안보다 더 나은 성능을 낼 수 있음을 시사합니다.

3.4 도메인별 변이

• 복소해석학은 컴파일 피드백으로부터 가장 높은 이득(+54.2 포인트)을 얻었으며, 이는 성숙한 Mathlib 커버리지 덕분인 것으로 보입니다.
• 실해석학과 대수학은 더 작은 이득을 보였는데, 이는 라이브러리 지원의 한계나 내재적인 정식화 난이도가 높음을 나타냅니다.
• 위상수학은 고급 개념(예: 피복 공간)과 관련된 특정 어려움을 보였으며, 여기서 피드백은 유효하지만 의미적으로 변화된 문장을 만드는 결과를 초래하곤 했습니다.

4. 의의 및 주장

본 논문은 문장 정식화가 단순히 Lean 수용 여부가 아니라 의미 보존으로서 평가되어야 한다고 주장합니다. 주요 기여는 다음과 같습니다:

1. 새로운 메트릭: "컴파일 통과 격차"를 드러내는 인간 보정된 합의 기반 메트릭을 제시하여, 많은 시스템이 구문적으로는 유효하지만 의미적으로는 틀린 문장을 생성한다는 점을 밝혀냈습니다.
2. 진단적 분해: 도구가 단조로운 추가 요소가 아님을 보여주는 요인 분석을 제공합니다. 피드백은 구문을 수정하지만 의미적 오류를 은폐할 수 있고, 검색은 근거 형성을 개선하지만 피드백이 있을 때는 한계 효용이 감소하며, 특화된 초안 작성은 피드백이 풍부한 루프 내에서 반드시 필요한 것은 아닙니다.
3. 시스템 비교: 현재의 증명 지향 모델이나 특화된 정식화 모델이 명시적인 문장 중심 훈련이나 도구 증강 프로토콜 없이는 그 증명 능력을 의미적으로 충실한 문장 생성으로 자동으로 전이시키지 못한다는 증거를 제시합니다.

저자들은 향후 시스템이 평균 정확도 향상에만 의존하기보다, 강력한 Lean 피드백과 의미적 평가, 그리고 언제 검색하고, 수정하고, 멈출지를 결정하는 정책을 결합해야 한다고 결론짓습니다. 본 논문은 자신의 메트릭이 동등성에 대한 형식적 증명이라고 주장하는 것을 피하며, 대신 시스템 비교를 위한 보수적이고 확장 가능한 결정 경계로 위치시킵니다.