[논문리뷰] Beyond Solver Verdicts: Generative Reward Models for Autoformalization본 논문은 신경기호주의(Neurosymbolic) 시스템에서 solver가 코드의 실행 가능성만을 보장할 뿐, 자연어 문제와 공식 언어 간의 정확한 의미적 대응을 보장하지 못한다는 근본적인 취약점을 다룹니다.#Review#Autoformalization#Generative Verification#Verdict-Preserving-Unfaithfulness#SMT Solver#Reward Modeling#Neurosymbolic Systems2026년 9월 10일댓글 수 로딩 중
[논문리뷰] 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일댓글 수 로딩 중
[논문리뷰] TheoremGraph: Bridging Formal and Informal Mathematics현대 수학 연구는 거대하고 파편화되어 있어 수학적 결과들의 의존성 구조를 명확히 파악하기 어렵습니다. 논문 저자들은 informal한 문헌(arXiv 등)이 주로 문서 수준의 인용에 의존하는 반면, formal 라이브러리(Lean 등)는 매우 제한된 범위 내에서만 세밀한 의존성을 관리한다는 한계를 지적합니다.#Review#Formal-Informal Mathematics#Dependency Graph#LeanGraph#Neural Theorem Proving#Cross-modal Retrieval#Autoformalization2026년 6월 29일댓글 수 로딩 중
[논문리뷰] miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward본 연구는 AI 시스템이 수학 올림피아드 문제에 참여하는 시나리오에서 miniF2F 벤치마크 의 비공식 및 공식 진술 간의 불일치와 오류를 분석하고 해결하는 것을 목표로 합니다.#Review#Automated Theorem Proving#Autoformalization#Benchmark Dataset#miniF2F#Lean Language#Large Language Models#Mathematical Reasoning#Formal Verification2025년 11월 16일댓글 수 로딩 중
[논문리뷰] ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization자연어 수학 문제를 기계 검증 가능한 형식적 진술로 변환하는 자동 형식화(Autoformalization) 과정에서 대규모 언어 모델(LLM) 이 원본 문제의 의미적 의도 를 정확히 보존하지 못하는 문제를 해결하는 것이 목표입니다.#Review#Autoformalization#Large Language Models#Reinforcement Learning#Self-Reflection#Semantic Consistency#Formal Mathematical Reasoning#Sequence Optimization2025년 10월 30일댓글 수 로딩 중