activity
20232025
most citedLEGO-Prover: Neural Theorem Proving with Growing Libraries

9 citations · 10 across the 6 of their papers we have counts for

collaborators

6 papers

cs.AI2025★ 1 cited

ORMind: A Cognitive-Inspired End-to-End Reasoning Framework for Operations Research

Zhiyuan Wang, Bokui Chen, Yinya Huang +4

Operations research (OR) is widely deployed to solve critical decision-making problems with complex objectives and constraints, impacting manufacturing, logistics, finance, and hea…

cs.AI2024

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…

cs.CL2024

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…

cs.AI2024

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…

cs.AI2023★ 9 cited

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…

cs.CL2023

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…