[논문리뷰] StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean본 논문은 기존의 수학 벤치마크들이 경쟁 수학(Competition Math) 문제에만 편중되어 있어, 실제 응용 수학 분야인 확률 과정 문제를 충분히 다루지 못한다는 한계를 해결하고자 합니다.#Review#Stochastic Processes#Lean 4#Automated Theorem Proving#Benchmark#Formalization#Markov Chains#Stochastic Calculus2026년 9월 9일댓글 수 로딩 중
[논문리뷰] MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement본 연구는 기존 autoformalization 모델들이 수학적 개념을 Mathlib의 복잡한 타입 시스템에 매핑하는 과정에서 겪는 한계와, 정적인 데이터 생성 방식의 구조적 문제를 해결하고자 합니다.#Review#Autoformalization#Lean 4#Knowledge Retrieval#Iterative Refinement#FormalVerse#Reinforcement Learning2026년 8월 18일댓글 수 로딩 중
[논문리뷰] FVSpec: Real-World Property-Based Tests as Lean Challenges본 논문은 AI 모델 및 에이전트의 실제 소프트웨어 형식 검증(formal software verification) 능력을 평가하기 위한 벤치마크 부족 문제를 해결하고자 합니다.#Review#Formal Verification#Property-Based Testing#Lean 4#LLM Pipeline#Benchmark#AI Safety#Structural Faithfulness2026년 6월 14일댓글 수 로딩 중
[논문리뷰] Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search본 논문은 LLM이 생성한 Lean 4 증명이 정답은 맞추지만, 지나치게 장황하고 특정 버전의 라이브러리에 취약하다는 점을 해결하고자 합니다 .#Review#Lean 4#Proof Optimization#Agentic Framework#Retrieval-Augmented Generation#Multi-Objective Optimization#Formal Verification2026년 5월 21일댓글 수 로딩 중
[논문리뷰] 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일댓글 수 로딩 중