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

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

collaborators
Showing 2024Show all

6 papers · 1 filter

cs.LG2024★ 1 cited

OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling

Zhicheng Yang, Yiwei Wang, Yinya Huang +7

Large language models (LLMs) have exhibited their problem-solving abilities in mathematical reasoning. Solving realistic optimization (OPT) problems in application scenarios requir…

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.AI2024

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…

cs.AI2024★ 6 cited

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

Huajian Xin, Daya Guo, Zhihong Shao +6

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathem…

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…