연구자들은 신경 정리 증명용 모듈식 완전 비동기 트리 검색을 위해 설계된 오픈소스 Python 라이브러리인 TreeThink를 소개했습니다. 이는 확립된 검색 방법과 vLLM 기반 추론 파이프라인, 다양한 노드 평가 기법을 통합합니다.
- Lean~4, Rocq, Isabelle/HOL 및 자연어 추론을 지원합니다.
- 실시간 검증 및 증명 상태 추출을 위해 각 언어의 REPL 서버에 직접 연결됩니다.
- miniF2F 및 MATH500 벤치마크에서 비동기 실행으로 최대 6.3배의 월클럭 속도 향상을 보여줍니다.
이 라이브러리는 교차 언어 형식 증명 검색 및 자연어 추론 지원을 가능하게 하며, 소스 코드는 MIT 라이선스 하에 공개되었습니다.