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