[논문리뷰] 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일댓글 수 로딩 중
[논문리뷰] Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics기존 에이전트 기반 형식 증명 시스템의 유연성, 재현성, 확장성 한계를 해결하고자 합니다.#Review#Agentic Systems#Formal Theorem Proving#Large Language Models (LLMs)#Lean Theorem Prover#Multi-Agent Systems#Code Generation#Automated Reasoning#Human-AI Collaboration2026년 1월 21일댓글 수 로딩 중
[논문리뷰] Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience본 논문은 학부 및 대학원 수준 이상의 수학 문제에 대한 형식적 정리 증명(Formal Theorem Proving)의 효율성과 성능을 개선하는 것을 목표로 합니다. 특히, LLM 기반의 형식적 증명에서 나타나는 높은 계산 비용과 도전 과제를 해결하며, 자연어 증명과 형식어 증명 간의 간극을 효과적으로 연결하고자 합니다.#Review#Formal Theorem Proving#Large Language Models#Reinforcement Learning#Agentic Prover#Lean Theorem Prover#Mathematical Reasoning#Test-Time Scaling2025년 12월 21일댓글 수 로딩 중