3 papers
cs.LO2025
Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
Zhenwen Liang, Linfeng Song, Yang Li +4
Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remain…
cs.AI2025
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
Zhenwen Liang, Linfeng Song, Yang Li +4
Automated Theorem Proving (ATP) in formal languages remains a formidable challenge in AI, demanding rigorous logical deduction and navigating vast search spaces. While large langua…
cs.AI2025
HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
Yang Li, Dong Du, Linfeng Song +4
We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a…