[논문리뷰] 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일댓글 수 로딩 중