← 返回论文库

AlphaProof / AlphaGeometry 2: Olympiad-level Formal Mathematical Reasoning with RL

DeepMind · 2024
L1 · Domain Research AgentsNature 643 (2025)#formal-math#verification#mcts
CORE IDEA
AlphaProof（AlphaZero MCTS + Lean kernel）+ AlphaGeometry 2（LLM 提辅助线 + 符号引擎），IMO 2024 银牌。
CONCRETE EXAMPLE
AlphaProof 解决 IMO 2024 P6，现场只 5 人解出。
L-ANCHOR · 为什么在这一层重要
neuro-symbolic verification 终极形式，verifier 可信度 = Lean kernel

相关论文

Navigating the Alpha Jungle: An LLM-Powered MCTS Framework for Formulaic Factor Mining
L0.32025
FunSearch: Mathematical Discoveries from Program Search with LLMs
L12023
AI Scientist v1: Towards Fully Automated Open-Ended Scientific Discovery
L12024
AI Scientist v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search
L12025