본 연구는 자연어에서 Lean 진술을 형식화하는 과정에서 컴파일만으로는 진술의 충실도를 판단하기 어렵다는 점을 지적해요. 400개의 대학원 수준 문제를 활용하여, 컴파일 성공률과 의미적 판단, 전문가 검증을 결합한 새로운 평가 프로토콜을 제시했어요. 결과적으로 도구 지원 에이전트는 89.5%의 컴파일 성공률을 보였지만, 충실도 합의는 60.5%에 불과했어요.
컴파일 성공률과 충실도 간의 29포인트 차이는 기존 평가 방식의 한계를 드러내며, 형식적 타당성, Lean 능력, 충실한 진술 생성의 중요성을 강조해요. 인간 전문가 검토 결과, 합의된 긍정 결과의 96%는 충실한 것으로 확인되었고, 컴파일 성공 후 의미적 실패는 82.4%에 달했어요.
다양한 개입 요소를 분석한 결과, Lean 세부 작업 피드백이 타당성을 가장 크게 개선했지만, 동시에 컴파일 성공 후 의미적 실패의 비율도 높였고, Mathlib 검색은 주로 맥락과 선택성을 향상시켰으며, 미세 조정된 초안 작성은 피드백과 맥락 검색이 가능해지면 대체 가능하다는 점을 발견했어요.