9 citations · 16 across the 16 of their papers we have counts for
16 papers
Prune-OPD: Efficient and Reliable On-Policy Distillation for Long-Horizon Reasoning
Zhicheng Yang, Zhijiang Guo, Yifan Song +5
On-policy distillation (OPD) leverages dense teacher rewards to enhance reasoning models. However, scaling OPD to long-horizon tasks exposes a critical flaw: as the student's gener…
Accordion-Thinking: Self-Regulated Step Summaries for Efficient and Readable LLM Reasoning
Zhicheng Yang, Zhijiang Guo, Yinya Huang +5
Scaling test-time compute via long Chain-of-Thought unlocks remarkable gains in reasoning capabilities, yet it faces practical limits due to the linear growth of KV cache and quadr…
Critique to Verify: Accurate and Honest Test-Time Scaling with RL-Trained Verifiers
Zhicheng Yang, Zhijiang Guo, Yinya Huang +4
Test-time scaling via solution sampling and aggregation has become a key paradigm for improving the reasoning performance of Large Language Models (LLMs). While reward model select…
TreeRPO: Tree Relative Policy Optimization
Zhicheng Yang, Zhijiang Guo, Yinya Huang +3
Large Language Models (LLMs) have shown remarkable reasoning capabilities through Reinforcement Learning with Verifiable Rewards (RLVR) methods. However, a key limitation of existi…
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
Junqi Liu, Xiaohan Lin, Jonas Bayer +12
Neurosymbolic approaches integrating large language models with formal reasoning have recently achieved human-level performance on mathematics competition problems in algebra, geom…
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…
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…
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…
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…
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…
CLOMO: Counterfactual Logical Modification with Large Language Models
Yinya Huang, Ruixin Hong, Hongming Zhang +6
In this study, we delve into the realm of counterfactual reasoning capabilities of large language models (LLMs). Our primary objective is to cultivate the counterfactual thought pr…
AlignedCoT: Prompting Large Language Models via Native-Speaking Demonstrations
Zhicheng Yang, Yinya Huang, Jing Xiong +4
Large Language Models prompting, such as using in-context demonstrations, is a mainstream technique for invoking LLMs to perform high-performance and solid complex reasoning (e.g.,…
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…
Discourse-Aware Graph Networks for Textual Logical Reasoning
Yinya Huang, Lemao Liu, Kun Xu +3
Textual logical reasoning, especially question-answering (QA) tasks with logical reasoning, requires awareness of particular logical structures. The passage-level logical relations…