LLM은 대화형 정리증명기에서 증명 공백을 메울 수 있지만, 검증된 정리가 곧 재사용 가능한 라이브러리 기여는 아니다. 연구진은 그로텐디크 소멸정리(Grothendieck's vanishing theorem)의 반자율 형식화를 사례로 이 차이를 분석한다. 초기 버전은 sorry 없이 컴파일됐으나 전문가 검토에서 정의, 정리의 일반성, 파일 구성, API에 심각한 문제가 발견됐다. 이후 검토 주도 리팩터·압축 과정을 거쳐 2차 전문가 검토를 받았다. 전후 비교 결과 뚜렷한 분기가 드러났는데, 에이전트는 국소적이고 기계적으로 검증 가능한 피드백에는 잘 적응했지만 정의 선택과 API 설계에는 여전히 취약했다. 저자들은 자동형식화를 닫힌 sorry 수만이 아니라 전문가 검토를 통과하는지로 평가해야 한다고 주장한다.
- •그로텐디크 소멸정리의 반자율 형식화를 사례로 검증된 정리와 재사용 가능한 라이브러리 기여의 차이를 분석
- •초기 버전은 sorry 없이 컴파일됐으나 정의·일반성·파일 구성·API에서 심각한 문제 발견
- •에이전트는 국소·기계 검증 가능한 피드백에는 잘 적응, 정의 선택과 API 설계에는 취약
- •자동형식화는 닫힌 sorry 수가 아닌 전문가 검토 통과 여부로 평가해야 함을 주장
Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
본문 미리보기
arXiv:2606.13925v1 Announce Type: new Abstract: Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this distinction through a detailed case study: a semi-autonomous formalization of Grothendieck's vanishing theorem. The initial version compiles with no sorries, but an expert review found serious problems in definitions, theorem generality, file organization, and the API. We th
전체 내용이 궁금하다면?
원문을 직접 읽어보세요