자동 정리 증명 시스템을 위한 최소 에이전트

A Minimal Agent for Automated Theorem Proving

본 논문에서는 다양한 AI 기반 정리 증명 시스템 아키텍처 간의 체계적인 비교를 가능하게 하는 최소 에이전트 기반 모델을 제안합니다. 이 모델은 최첨단 시스템에서 공유하는 핵심 기능, 즉 반복적인 증명 개선, 라이브러리 검색 및 컨텍스트 관리를 구현합니다. 우리는 질적으로 다른 벤치마크를 사용하여 이 기반 모델을 평가하고, 다양한 인기 모델과 설계 방식을 비교하며, 최첨단 접근 방식과 경쟁력 있는 성능을 보이면서도 훨씬 간단한 아키텍처를 사용함을 입증합니다. 우리의 결과는 반복적인 접근 방식이 여러 번의 단일 실행 생성 방식보다 샘플 효율성과 비용 효율성 측면에서 일관된 장점을 제공한다는 것을 보여줍니다. 이 구현은 향후 연구를 위한 참조 모델 및 커뮤니티를 위한 접근 가능한 증명 시스템으로 오픈 소스로 공개됩니다.

We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate our baseline using qualitatively different benchmarks and compare various popular models and design choices, and demonstrate competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture. Our results demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.