Zhengying Liu

Moonshot AI

LIU Zhengying is a researcher at Moonshot AI (Kimi), focusing on large language models (LLMs) and AI for Math. He led the Kimina series project in collaboration with Numina and participated in the development of the Kimi K2 series. Since 2016, he has been in pursuit of enabling AI to perform superhuman mathematical intelligence. From 2021 to 2024, he led projects on neural theorem proving and AI Agents at Huawei Noah's Ark Lab, with publications at NeurIPS, ACL, ICLR, etc. He obtained his Ph.D. in artificial intelligence from Université Paris-Saclay, advised by Isabelle Guyon, specializing in automated deep learning. He obtained his Master degree in both fundamental mathematics and computer science from Ecole polytechnique and a Bachelor's degree in both physics and mathematics from Peking University's Yuanpei College.

Talk

Title: Kimina-Prover: A Large Formal Reasoning Model Based on Reinforcement Learning

Abstract: Kimina-Prover is the first large formal reasoning model, jointly developed by Numina and Moonshot AI. It can reason in a human-like manner and rigorously prove mathematical theorems in the structured language Lean 4. Building on the reinforcement learning pipeline of Kimi k1.5 and incorporating a proposed formal reasoning pattern, Kimina-Prover significantly improves proof efficiency and achieves an accuracy rate of over 80% on the standard miniF2F benchmark for the first time. The model generates full proofs without prover feedback, demonstrating strong performance consistent with Kimi k1.5, without relying on complex techniques such as Monte Carlo tree search or value functions. Experiments show that model performance scales significantly with size (e.g., 72B), a trend previously unobserved in neural theorem provers. Additionally, the model uses the longest context window of up to 32K tokens for training and inference and designs a unique “Formal Reasoning Pattern” to bridge the gap between formal verification and informal mathematical intuition.