Lean 4의 형식 검증과 대규모언어모델 에이전트를 결합한 오픈소스 자동 정리 증명 시스템 OpenProver가 공개됐다. 수학 문제를 여러 하위 문제로 나누고 병렬로 탐색하면서, 생성된 증명을 Lean 커널로 확인해 재현 가능한 평가를 제공하는 것이 목표다.
구조는 Planner-Worker-Verifier로 나뉜다. Planner는 짧은 화이트보드와 중간 발견을 제한 없이 저장하는 저장소를 관리하고, 수학 작업을 여러 Worker에 배분한다. Verifier는 후보 증명이 Lean 4에서 실제로 통과하는지 검사해 자연어 평가자의 주관을 줄인다.
대화형 터미널 모드에서는 사람이 증명 탐색을 관찰하고 방향을 수정할 수 있다. 연구진은 자동 형식 검증 덕분에 구성요소를 제거해 영향을 비교하는 정량 실험이 가능하다고 설명하고, ProofNet에서 단순 기준선과 비교한 평가를 제시했다. 그러나 초록에는 성공률이나 계산 비용의 절대 수치가 없다.
Lean이 수용한 증명은 형식적 정확성을 강하게 보장하지만, 정리의 전제가 현실 문제를 올바르게 표현했는지까지 확인하지는 않는다. Planner의 저장소가 길어질 때의 검색 비용, 병렬 Worker의 모델 호출량, ProofNet 밖의 고난도 정리에서의 성능도 별도 평가가 필요하다.
OpenProver 논문은 2026년 7월 arXiv에 공개된 시스템 프리프린트로 동료검토 전이며 코드는 공개 저장소로 제공됐다. 현재 확인되는 성과는 완전 공개 구조와 Lean 검증·사람 개입을 한 시스템에 묶었다는 점이다. 다른 정리군과 모델에서도 같은 효과가 나는지는 확인이 필요하다. 공개 환경에서의 재현 결과가 축적돼야 적용 범위를 판단할 수 있다.
저작권자 © STORIUM 무단전재 및 재배포 금지
