Visored: LLM이 생성한 수학을 위한 제어된 자연어 증명기 (Controlled-Natural-Language Prover)

우리는 LLM(Large Language Models)과 인간이 수학을 작성하는 방식에 맞춰 설계된 의존 타입 기반(dependent-type-based) 증명기를 제시하며, 이는 Lean 및 Rocq와 같은 기존 시스템을 보완합니다. 이 시스템의 핵심 설계 선택 사항은 수학적 자연어(mathematical natural language)를 모방하는 표면층(surface)과, 교과서에서 생략될 법한 일상적인 단계들을 처리하는 규칙 기반 자동화 계층(rule-driven automation layer)입니다. 이를 통해 승인된 증명은 검증된 Lean 파일로 다시 출력될 수 있습니다. 초기 실험 결과에 따르면, 증명기 전용 학습 데이터가 없는 상태에서도 LLM은 miniF2F 벤치마크에서 이를 효과적으로 사용하는 법을 배울 수 있음을 시사합니다. Lean 출력 발췌본: https://github.com/xiyuzhai-husky-lang/visored/