점근 통계 이론은 수렴 진술, 점근 전개, 함수해석학, 정칙성 조건이 뒤섞여 Lean 4 형식화 인프라와 큰 격차가 있어 AI 보조 형식화에 어렵다. 저자는 증명 계획·골격 구성·Mathlib 정찰·증명 구축·통합·독립 검토·감사의 일곱 전문 역할을 관리자가 조율하는 다중 에이전트 Lean 4 형식화 파이프라인을 제안한다. 핵심 규율은 감사자(Auditor) 에이전트가 수행하는 가설 규율 감사로, 모든 주정리 가설과 개념 계층 필드를 원문 수학 서술에 근거시키거나 Lean 인코딩 어댑터로 정당화하거나 원문 함의로 표시하거나 근거 없는 강화로 기각한다. 이 워크플로로 모수·준모수 모형의 점근 분포·효율 결과를 공리 청정하고 원문 충실하게 형식화했다.
- •일곱 전문 역할을 관리자가 조율하는 다중 에이전트 Lean 4 형식화 파이프라인을 제안한다.
- •감사자 에이전트가 모든 가설을 원문에 근거시키거나 어댑터로 정당화·기각하는 가설 규율 감사를 적용한다.
- •모수·준모수 모형의 점근 분포·효율 결과를 공리 청정·원문 충실하게 형식화했다.
- •정리 비의존 인프라와 통계 개념 정의를 정리별 조립과 분리해 구성했다.
Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
본문 미리보기
arXiv:2606.20642v1 Announce Type: new Abstract: Asymptotic statistical theory is a challenging domain for AI-assisted formalization: its central results mix convergence statements, asymptotic expansions, functional analysis, and regularity conditions that have a large gap from existing infrastructure in Lean 4 formalization. To address these challenges, we propose a hypothesis-disciplined Lean 4 formalization pipeline built from multiple agents: a manager that coordinates seven specialist roles
전체 내용이 궁금하다면?
원문을 직접 읽어보세요