연구진이 에이전트 기반 형식적 정리 증명 프레임워크 OProver를 공개했어요. OProver는 실패한 증명 시도를 반복적으로 수정하며, 컴파일러 검증 증명과 Lean 컴파일러 피드백을 활용합니다.
OProver는 지속적인 사전 훈련과 반복적인 사후 훈련을 거치며, 177만 개의 Lean 문장, 686만 개의 컴파일러 검증 증명, 그리고 다양한 시도 기록을 포함하는 OProofs 데이터셋을 구축했어요.
다섯 가지 벤치마크에서 OProver-32B는 MiniF2F, ProverBench, PutnamBench에서 최고 Pass@32 점수를 달성하며, 기존 오픈 웨이트 전체 증명 프로버보다 더 높은 성과를 보였어요.