13 papers
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu +11
Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction an…
Training LLMs for Divide-and-Conquer Reasoning Elevates Test-Time Scalability
Xiao Liang, Zhong-Zhi Li, Zhenghao Lin +7
Large language models (LLMs) have demonstrated strong reasoning capabilities through step-by-step chain-of-thought (CoT) reasoning. Nevertheless, at the limits of model capability,…
Beyond Pass@1: Self-Play with Variational Problem Synthesis Sustains RLVR
Xiao Liang, Zhongzhi Li, Yeyun Gong +4
Reinforcement Learning with Verifiable Rewards (RLVR) has recently emerged as a key paradigm for post-training Large Language Models (LLMs), particularly for complex reasoning task…
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
Boyan Duan, Xiao Liang, Shuai Lu +7
Automated theorem proving in Euclidean geometry, particularly for International Mathematical Olympiad (IMO) level problems, remains a major challenge and an important research focu…
Mixture of Neuron Experts
Runxi Cheng, Yuchen Guan, Yucheng Ding +6
In this work, we first explore whether the parameters activated by the MoE layer remain highly sparse at inference. We perform a sparsification study on several representative MoE…
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu +10
Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generatio…