28 citations · 55 across the 14 of their papers we have counts for
14 papers
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Haiming Wang, Mert Unsal, Xiaohan Lin +37
We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview rele…
FormalAlign: Automated Alignment Evaluation for Autoformalization
Jianqiao Lu, Yingjia Wan, Yinya Huang +3
Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic al…
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
Xiaohan Lin, Qingxing Cao, Yinya Huang +5
Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs). However, current formal verificati…
Process-Driven Autoformalization in Lean 4
Jianqiao Lu, Yingjia Wan, Zhengying Liu +10
Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing effort…
Proving Theorems Recursively
Haiming Wang, Huajian Xin, Zhengying Liu +8
Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually base…
ATG: Benchmarking Automated Theorem Generation for Generative Language Models
Xiaohan Lin, Qingxing Cao, Yinya Huang +4
Humans can develop new theorems to explore broader and more complex mathematical results. While current generative language models (LMs) have achieved significant improvement in au…
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
Yinya Huang, Xiaohan Lin, Zhengying Liu +6
Recent large language models (LLMs) have witnessed significant advancement in various tasks, including mathematical reasoning and theorem proving. As these two tasks require strict…
Large Language Models as Automated Aligners for benchmarking Vision-Language Models
Yuanfeng Ji, Chongjian Ge, Weikai Kong +4
With the advancements in Large Language Models (LLMs), Vision-Language Models (VLMs) have reached a new level of sophistication, showing notable competence in executing intricate c…
LEGO-Prover: Neural Theorem Proving with Growing Libraries
Haiming Wang, Huajian Xin, Chuanyang Zheng +11
Despite the success of large language models (LLMs), the task of theorem proving still remains one of the hardest reasoning tasks that is far from being fully solved. Prior methods…
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
Jing Xiong, Jianhao Shen, Ye Yuan +11
Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchma…
Gaining Wisdom from Setbacks: Aligning Large Language Models via Mistake Analysis
Kai Chen, Chunwei Wang, Kuo Yang +11
The rapid development of large language models (LLMs) has not only provided numerous opportunities but also presented significant challenges. This becomes particularly evident when…
Lyra: Orchestrating Dual Correction in Automated Theorem Proving
Chuanyang Zheng, Haiming Wang, Enze Xie +6
Large Language Models (LLMs) present an intriguing avenue for exploration in the field of formal theorem proving. Nevertheless, their full potential, particularly concerning the mi…
MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models
Longhui Yu, Weisen Jiang, Han Shi +7
Large language models (LLMs) have pushed the limits of natural language understanding and exhibited excellent problem-solving ability. Despite the great success, most existing open…
FIMO: A Challenge Formal Dataset for Automated Theorem Proving
Chengwu Liu, Jianhao Shen, Huajian Xin +9
We present FIMO, an innovative dataset comprising formal mathematical problem statements sourced from the International Mathematical Olympiad (IMO) Shortlisted Problems. Designed t…