[논문리뷰] LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning최근 Large Language Models (LLMs)의 추론 능력 향상에도 불구하고, 현재 LLMs는 Lean4 와 같이 엄격하고 검증된 formal language를 요구하는 formal theorem-proving task에서 여전히 어려움을 겪고 있다.#Review#Mixture-of-Experts#Native Formal Reasoning#Tool-Integrated Reinforcement Learning#Lean4#Auto-formalization#Theorem Proving#Hierarchical Importance Sampling Policy Optimization2026년 3월 23일댓글 수 로딩 중
[논문리뷰] s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs본 논문은 LLM이 산업용 cryptographic assembly 코드를 검증할 수 있는지를 평가하기 위해, AWS의 s2n-bignum 라이브러리에서 추출한 형식 명세와 HOL Light 증명 스크립트 생성 과제를 묶은 실용 벤치마크를 제안합니다.#Review#Formal Verification#Theorem Proving#HOL Light#LLM for Code#Cryptographic Assembly#Neurosymbolic AI2026년 3월 22일댓글 수 로딩 중
[논문리뷰] Towards Autonomous Mathematics Research본 논문은 국제 수학 올림피아드(IMO) 수준을 넘어 전문적인 수학 연구 영역으로 AI의 능력을 확장하는 것을 목표로 합니다. 방대한 문헌 탐색과 장기적인 증명 구성이 요구되는 연구 문제 해결을 위해, 자연어로 솔루션을 반복적으로 생성, 검증, 수정하는 수학 연구 에이전트 Aletheia 를 소개합니다.#Review#Mathematics Research#Large Language Models#AI Agents#Theorem Proving#Tool Use#Gemini Deep Think#Autonomous Research#Human-AI Collaboration2026년 2월 11일댓글 수 로딩 중
[논문리뷰] DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning대규모 언어 모델(LLM)이 수학적 추론에서 최종 정답 기반 보상의 한계를 가지며, 이는 증명 작업에 적용하기 어렵고 추론의 정확성을 보장하지 못한다는 문제점을 해결하고자 합니다.#Review#Mathematical Reasoning#Large Language Models (LLMs)#Proof Verification#Self-Verification#Reinforcement Learning (RL)#Theorem Proving#Meta-Verification#Iterative Refinement2025년 11월 30일댓글 수 로딩 중