10 papers
Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
Joshua Ong Jun Leang, Haonan Li, Zheng Zhao +7
Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in usi…
Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5
Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning tra…
CoLVR: Enhancing Exploratory Latent Visual Reasoning via Contrastive Optimization
Ziyang Ding, Linjian Meng, Yiming Wu +3
Due to the potential for exploratory reasoning of Latent Visual Reasoning, recent works tend to enable MLLMs (Multimodal Large Language Models) to perform visual reasoning by propa…
Training with Harnesses: On-Policy Harness Self-Distillation for Complex Reasoning
Zhengyang Zhao, Lu Ma, Wentao Zhang
Inference-time harnesses substantially improve large language models on complex reasoning tasks. However, the intrinsic capabilities of the underlying model remain unchanged by the…
CodeCircuit: Toward Inferring LLM-Generated Code Correctness via Attribution Graphs
Yicheng He, Zheng Zhao, Zhou Kaiyu +3
Current paradigms for code verification rely heavily on external mechanisms-such as execution-based unit tests or auxiliary LLM judges-which are often labor-intensive or limited by…
GIFT: Reconciling Post-Training Objectives via Variational Finite-Temperature Gibbs Initialization
Zhengyang Zhao, Lu Ma, Yizhen Jiang +7
The prevailing post-training paradigm for Large Reasoning Models (LRMs)---Supervised Fine-Tuning (SFT) followed by Reinforcement Learning (RL)-suffers from an intrinsic optimizatio…