[논문리뷰] LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning최근 Large Language Models (LLMs)의 추론 능력 향상에도 불구하고, 현재 LLMs는 Lean4 와 같이 엄격하고 검증된 formal language를 요구하는 formal theorem-proving task에서 여전히 어려움을 겪고 있다.#Review#Mixture-of-Experts#Native Formal Reasoning#Tool-Integrated Reinforcement Learning#Lean4#Auto-formalization#Theorem Proving#Hierarchical Importance Sampling Policy Optimization2026년 3월 23일댓글 수 로딩 중