자연어를 Lean 형식 명제로 옮기는 '충실한(faithful) 형식화'를 평가·병목 규명 문제로 다룬 연구다. 컴파일 통과는 타당성 검사일 뿐, 가설을 빠뜨리거나 도메인을 바꾸거나 공허한 주장을 만들어도 타입체크는 통과할 수 있다. 실해석·복소해석·위상수학·대수 400문항 대학원급 벤치마크에서 Lean 컴파일, 교차 모델 의미 판정, 인간 전문가 보정을 결합한 결과, 완전 도구 증강 에이전트는 컴파일률 89.5%에 도달했지만 합의 충실도는 60.5%에 그쳐 29.0%p 격차를 드러냈다. 인간 감사에서 합의 긍정 출력의 96.0%가 충실 확인, 컴파일 통과·합의 부정 출력의 82.4%가 의미 실패로 확인됐다. 2^3 요인 설계 분석에서 elaboration 피드백이 최대 타당성 개선이나 의미 실패도 늘렸고, 검색은 근거·선택성을, 파인튜닝 초안은 대체 가능함을 보였다.
- •컴파일 통과는 타당성 검사일 뿐, 가설 누락·도메인 변경·공허한 주장도 타입체크를 통과할 수 있음
- •도구 증강 에이전트가 컴파일률 89.5% vs 합의 충실도 60.5%로 29.0%p 격차 노출
- •인간 감사: 합의 긍정 출력의 96.0%가 충실, 컴파일 통과·합의 부정 출력의 82.4%가 의미 실패로 확인
- •2^3 요인 분석: elaboration 피드백이 최대 타당성 개선이나 의미 실패도 증가, 검색은 근거·선택성 개선
0단 자동
AI가 규칙대로 쓰고 그대로 게시했습니다. 사람이 따로 보지 않았습니다.
- 규칙 판
- 규칙 판 도입 이전 기사입니다.
- 남기는 것
- 규칙 판 · 모델 · 시각
- 판 기록
- 아직 없습니다.
Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
- 1.자연어-Lean 형식화에서 컴파일 통과가 아닌 '충실한 명제 생성'을 평가하는 프로토콜 제안
- 2.400개 대학원 수준 벤치마크에서 도구 증강 에이전트가 컴파일 89.5% vs 충실도 60.5%로 29점 격차 노출
- 3.합의 긍정 출력의 96.0%가 인간 확인 충실, 컴파일 통과지만 합의 부정인 출력의 82.4%는 의미 오류
- 4.2^3 요인 설계로 엘라보레이션 피드백이 최대 유효성 개입임을 분해 분석
왜 중요한가?
정리증명 벤치마크가 고정된 형식 명제에 의존하던 것과 달리, 형식화 자체의 의미 충실도를 컴파일률과 분리해 측정해야 함을 드러낸다. 컴파일은 통과해도 가설 누락·영역 변경·공허한 명제가 가능하다는 점에서, 형식화 파이프라인 평가 기준을 재정립한다.
본문 미리보기
arXiv:2606.31002v1 Announce Type: new Abstract: Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check while omitting hypotheses, changing domains, or expressing a vacuous claim. We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem. On a 400
전체 내용이 궁금하다면?
원문을 직접 읽어보세요
이 글이 만들어진 과정
- 13:08AI 초안
