12 papers
Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning
Ji Feng, Zhouxing Shi
With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-che…
Evaluating the Robustness of Proof Autoformalization in Lean 4
Zhengtao Gui, Sheng Yang, Zhouxing Shi
Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have deve…
GRLO: Towards Generalizable Reinforcement Learning in Open-Ended Environments from Zero
Shangjian Yin, Yu Fu, Yue Dong +1
Post-training has become a crucial step for unlocking the capabilities of large language models, with reinforcement learning (RL) emerging as a critical paradigm. Recent RL-based p…
PIKA: Expert-Level Synthetic Datasets for Post-Training Alignment from Scratch
Shangjian Yin, Shining Liang, Wenbiao Ding +4
High-quality instruction data is critical for LLM alignment, yet existing open-source datasets often lack efficiency, requiring hundreds of thousands of examples to approach propri…
Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control
Zhouxing Shi, Haoyu Li, Cho-Jui Hsieh +1
We study the problem of learning verifiably Lyapunov-stable neural controllers that provably satisfy the Lyapunov asymptotic stability condition within a region-of-attraction (ROA)…
Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
Yizhak Y. Elboher, Reuven Peleg, Zhouxing Shi +2
Neural network verification tools currently support only a narrow class of specifications, typically expressed as low-level constraints over raw inputs and outputs. This limitation…