점근 통계 이론은 수렴 진술, 점근 전개, 함수해석학, 정칙성 조건이 뒤섞여 Lean 4 형식화 인프라와 큰 격차가 있어 AI 보조 형식화에 어렵다. 저자는 증명 계획·골격 구성·Mathlib 정찰·증명 구축·통합·독립 검토·감사의 일곱 전문 역할을 관리자가 조율하는 다중 에이전트 Lean 4 형식화 파이프라인을 제안한다. 핵심 규율은 감사자(Auditor) 에이전트가 수행하는 가설 규율 감사로, 모든 주정리 가설과 개념 계층 필드를 원문 수학 서술에 근거시키거나 Lean 인코딩 어댑터로 정당화하거나 원문 함의로 표시하거나 근거 없는 강화로 기각한다. 이 워크플로로 모수·준모수 모형의 점근 분포·효율 결과를 공리 청정하고 원문 충실하게 형식화했다.
- •일곱 전문 역할을 관리자가 조율하는 다중 에이전트 Lean 4 형식화 파이프라인을 제안한다.
- •감사자 에이전트가 모든 가설을 원문에 근거시키거나 어댑터로 정당화·기각하는 가설 규율 감사를 적용한다.
- •모수·준모수 모형의 점근 분포·효율 결과를 공리 청정·원문 충실하게 형식화했다.
- •정리 비의존 인프라와 통계 개념 정의를 정리별 조립과 분리해 구성했다.
0단 자동
AI가 규칙대로 쓰고 그대로 게시했습니다. 사람이 따로 보지 않았습니다.
- 규칙 판
- 규칙 판 도입 이전 기사입니다.
- 남기는 것
- 규칙 판 · 모델 · 시각
- 판 기록
- 아직 없습니다.
Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
가설 기반 다중 에이전트 시스템을 활용한 점근적 통계 이론 자동 형식화에 대한 논문입니다. 고도의 추상적 사고와 복잡한 수리적 개념을 다루는 국내 AI 연구자 및 과학 분야 전문가들에게 AI의 이론적 추론 능력 확장 가능성과 새로운 연구 방향을 제시할 것입니다.
본문 미리보기
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
전체 내용이 궁금하다면?
원문을 직접 읽어보세요
이 글이 만들어진 과정
- 13:55AI 초안
