[논문리뷰] 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일댓글 수 로딩 중
[논문리뷰] EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving논문은 LLM 기반의 Automated Theorem Proving(ATP) 모델들이 Chain-of-Thought (CoT) 추론 및 다중 샘플링 패스 와 같은 test-time scaling 전략을 사용하며 발생하는 높은 계산 비용과 자원 비효율성을 해결하는 것을 목표로 합니다.#Review#Automated Theorem Proving#LLM#Test-Time Scaling#Chain-of-Thought#Reinforcement Learning#Efficiency Optimization#Token Cost#Sampling Cost#Dynamic CoT Switching2025년 9월 17일댓글 수 로딩 중
[논문리뷰] Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem대규모 언어 모델(LLM)의 수학적 추론 능력 향상을 저해하는 고품질, 논리적으로 건전한 데이터의 부족 문제를 해결하는 것이 주된 목표입니다. 수십 년간의 자동화된 정리 증명(ATP) 연구를 확장 가능한 데이터 엔진으로 전환하여 LLM의 학습을 위한 대규모의 검증된 수학적 명제 및 추론 태스크 코퍼스를 생성하고자 합니다.#Review#Automated Theorem Proving#LLM#Mathematical Reasoning#Synthetic Data Generation#TPTP Ecosystem#Saturation Proving#Proof Graph Reconstruction#Data Augmentation2025년 9월 9일댓글 수 로딩 중
[논문리뷰] Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction본 논문은 형식 증명 자동화(Automated Theorem Proving, ATP) 분야에서 기존의 대규모 모델 및 연산량 의존성을 극복하고, 더 적은 자원으로도 최첨단 성능을 달성하는 새로운 오픈소스 언어 모델 시리즈인 Goedel-Prover-V2 를 개발하는 것을 목표로 합니다.#Review#Automated Theorem Proving#Formal Verification#Language Models#Self-Correction#Data Synthesis#Reinforcement Learning#Model Averaging#Lean2025년 8월 6일댓글 수 로딩 중
[논문리뷰] Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving본 논문은 대규모 언어 모델(LLM)이 자연어 기반 정리 증명에서 명확한 감독 신호 부족으로 겪는 어려움을 해결하고자 합니다.#Review#Automated Theorem Proving#Large Language Models#Formal Verification#Reinforcement Learning#Lean#Geometry Reasoning#Chain-of-Thought#Lemma-Style Proving2025년 8월 2일댓글 수 로딩 중
[논문리뷰] EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty본 논문은 형식적 정리 증명(formal theorem proving) 분야에서 대규모 언어 모델(LLMs) 의 일반화 능력이 부족하고 문제 진술의 사소한 변화에도 취약하다는 한계를 해결하는 것을 목표로 합니다.#Review#Automated Theorem Proving#Data Augmentation#Large Language Models#Formal Mathematics#Symmetry#Difficulty Evolution#Abstract Syntax Tree#Generalizability2025년 10월 7일댓글 수 로딩 중