[논문리뷰] OProver: A Unified Framework for Agentic Formal Theorem Proving본 논문은 기존 formal theorem proving 시스템이 증명 실패 시의 feedback과 retrieval을 inference-time heuristic으로만 사용하여 학습과 추론 간의 불일치(mismatch)가 발생하는 문제를 해결하고자 합니다.#Review#Formal Theorem Proving#Lean 4#Agentic Proving#Compiler Feedback#Test-Time Refinement#Reinforcement Learning2026년 5월 18일댓글 수 로딩 중