컨텍스트 내 학습 에이전트를 활용한 공리적 정리 증명

우리는 Lean 및 Coq과 같은 환경에서 형식적 정리 증명을 위한 인컨텍스트 학습 에이전트를 제안한다. 현재 이 문제에 대한 최상위 수준 모델들은 환경에 특화된 증명 데이터로 미세조정(finetuned)되어 있다. 반면에, 본 연구에서 제안하는 접근법인 COPRA는 상태를 유지하는 백트래킹 검색 내에서 고용량의 일반 목적 대규모 언어 모델(GPT-4)에게 전략(tactic) 적용을 반복적으로 제안하도록 요청한다. 제안된 전략은 기반 증명 환경에서 실행되며, 실행 결과로부터 피드백을 얻어 다음 모델 쿼리의 프롬프트를 구성한다. 이 과정에서 검색 기록에서 선택된 정보와 외부 데이터베이스에서 검색한 보조 정리(lemmas)도 함께 활용된다. 우리는 COPRA의 구현을 Lean용 miniF2F 벤치마크와 CompCert 프로젝트에서 가져온 Coq 작업 세트에 대해 평가하였다. 이러한 벤치마크에서 COPRA는 GPT-4의 희소 샘플(few-shot) 호출보다 뚜렷하게 우수한 성능을 보였다. 또한, 미세조정 기반 접근법들과 비교했을 때도 유리한 성과를 나타내었으며, Lean 분야에서 최상위 수준의 미세조정 모델인 ReProver보다 pass@1 지표에서 뛰어난 성능을 기록하였다. 본 연구의 코드와 데이터는 https://github.com/trishullab/copra 에 공개되어 있다.