정리 증명 (Theorem-proving) 벤치마크는 고정된 정식 문장 (formal statements)을 대상으로 증명 탐색을 평가하지만, 자연어-to-Lean 정식화 (natural-language-to-Lean formalization)는 정식 문장 자체를 생성해야 합니다. 이러한 설정에서 컴파일 (compilation)은 단지 유효성 검사 (validity check)일 뿐입니다. 즉, Lean 선언 (Lean declaration)이 가설을 누락하거나, 도메인을 변경하거나, 공허한 주장 (vacuous claim)을 표현하더라도 타입 체크 (type-check)를 통과할 수 있습니다. 우리는 충실한 문장 정식화 (faithful statement formalization)를 평가 문제이자 병목 현상 원인 규명 (bottleneck-attribution) 문제로서 연구합니다. 실해석학 (real analysis), 복소해석학 (complex analysis), 위상수학 (topology), 대수학 (algebra)을 아우르는 400개의 항목으로 구성된 대학원 수준의 벤치마크에서, 우리의 프로토콜은 Lean 컴파일, 모델 간 교차 의미론적 판정 (cross-model semantic judging), 그리고 인간 전문가 보정 (human expert calibration)을 결합합니다. 그 결과는 컴파일 성공률 (compile-rate) 평가와는 다른 양상을 보입니다. 도구 증강 에이전트 (tool-augmented agent)를 완전히 사용했을 때 컴파일 성공률은 89.5%에 달하지만, 합의된 충실도 (consensus faithfulness)는 60.5%에 불과하여, 컴파일은 통과했으나 합의된 충실도는 낮은 29.0%포인트의 격차를 드러냈습니다. 표적화된 인간 감사 (human audits)는 이 지표가 보수적인 결정 경계 (decision boundary)로서 유효함을 뒷받침합니다. 가용한 사례 수준 감사 결과, 합의된 긍정적 (consensus-positive) 출력의 96.0%가 인간에 의해 충실한 것으로 확인된 반면, 컴파일은 통과했으나 합의된 부정적 (consensus-negative)인 출력의 82.4%는 인간에 의해 의미론적 실패 (semantic failures)로 확인되었습니다. 이 지표 하에서 기존의 원샷 정식화 모델 (one-shot formalizer models)과 증명 중심의 Lean 모델들은 여전히 낮은 성능을 보이며, 이는 정식 유효성 (formal validity), 증명 중심의 Lean 역량 (proof-oriented Lean competence), 그리고 충실한 문장 생성 (faithful statement generation)이 각각 별도로 보고되어야 함을 시사합니다. 이후 우리는 $2^3$ 요인 설계 (factorial design)를 사용하여 정식화 파이프라인에서 반복되는 세 가지 개입 (interventions)을 분해합니다: 매개변수적 전문가 초안 작성 (parametric expert drafting), Mathlib/컨텍스트 검색 (context search), 그리고 Lean 정교화 피드백 (Lean elaboration feedback). 정교화 피드백은 가장 큰 유효성 개입 요소이지만, 동시에 컴파일은 통과했으나 의미론적으로 실패한 더 큰 범주를 노출합니다. 검색은 주로 근거 제시 (grounding)와 선택성 (selectivity)을 개선하며, 미세 조정된 초안 작성 (fine-tuned drafting)은 피드백과 근거 제시가 확보된 이 도구 스택 내에서는 대체 가능한 수준입니다.