OpenProver는 Lean 4 형식 검증을 통합한 LLM 기반 자동 정리 증명(ATP) 오픈소스 시스템이다. Aletheia 같은 최근 ATP 에이전트 시스템에서 영감을 받은 Planner-Worker-Verifier 아키텍처를 채택해, Planner 에이전트가 간결한 Whiteboard 스크래치패드와 무제한 Repository로 중간 결과를 관리하며 수학 작업을 병렬 Worker들에 분배한다. 생성된 증명을 자동 형식 검증해 재현 가능한 평가를 제공하고, 인간 운영자가 증명 탐색을 모니터링·조종할 수 있는 대화형 터미널 인터페이스도 지원한다. ProofNet에서 베이스라인과 비교 평가해 정량적 어블레이션 실험 가능성을 보였으며, GitHub에 전체 공개돼 인간-AI 협업형 정리 증명 연구의 재현 가능한 기반을 제공한다.
- •Planner-Worker-Verifier 구조에 Whiteboard·Repository로 중간 결과 관리
- •Lean 4 자동 형식 검증으로 재현 가능한 평가 지원
- •인간이 증명 탐색을 모니터링·조종하는 대화형 터미널 모드 제공
- •ProofNet 평가와 함께 GitHub에 완전 오픈소스로 공개
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
본문 미리보기
arXiv:2607.09217v1 Announce Type: new Abstract: In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates a Planner-Worker-Verifier architecture inspired by recent ATP agentic systems such as Aletheia. A Planner agent maintains a compact Whiteboard scratchpad and an unbounded Repository of intermediate findings, and decomposes mathematical work into parallel Workers. OpenP
전체 내용이 궁금하다면?
원문을 직접 읽어보세요