PaperFormalizer: Lean 환경에서 연구 논문의 저자 참여형 자동 형식화

arXiv:2610.31810v1 발표 유형: 신규 초록: 심지어 꼼꼼히 교정된 논문이라도 증명 과정이나 명시된 가정에 작은 허점이 남아 있을 수 있습니다. 우리는 PaperFormalizer를 소개합니다. 이는 Lean 기반의 에이전트형 파이프라인으로, 저자들이 자신의 논문에서 이러한 허점을 찾아 이를 보완하고, 각 논문을 Lean으로 검증된 버전으로 전환할 수 있도록 지원합니다. LaTeX 소스를 기반으로 PaperFormalizer는 논문을 명제들의 의존 관계 그래프로 변환한 뒤, 각 명제를 자연어로 검토하여 충실성, 모호성 및 정확성을 평가하고, 이후 Lean 언어로 명제들을 형식화하여 Mathlib, 선택적 도메인 라이브러리 및 저자의 개인 도구 세트와 비교해 증명합니다. 어떤 명제가 무엇을 의미하는지, 그리고 결과에 존재하는 형식화상의 허점을 어떻게 가장 잘 해결해야 하는지는 오직 저자만이 알고 있습니다. 따라서 이 파이프라인은 중단되어 저자에게 질문을 던집니다…