LEAP은 일반 LLM을 Lean 검증 루프 안의 형식 증명 에이전트로 바꾼다

arXiv 2606.03303은 전문 theorem prover fine-tuning보다 blueprint, AND-OR DAG, Lean compiler feedback을 결합한 agentic formal pr...