Bootstrapping Hierarchical Autoregressive Formal Reasoner with Chain-of-Proxy-Autoformalization
Qi Liu, Xinhao Zheng, Renqiu Xia, Qinxiang Cao, Junchi Yan
Deductive formal problem-solving (D-FPS) enables process-verified, human-aligned problem-solving by implementing deductive solving processes within formal theorem proving (FTP) environments. However, current methods fail to address the misalignment between informal and formal reasoning granularity, and suffer from inefficiency due to backtracking and error propagation. Moreover, the extreme scarcity of formal problem-solution pairs further hinders progress.For the first gap, we propose **HAR** (_**H**ierarchical **A**utoregressive Formal **R**easoner_), a novel reasoning pipeline. HAR decouples informal-aligned drafting and detailed proving, and formulates solution construction as autoregressive generation with per-step feedback. Second, we propose **CoPA** (_**C**hain-**o**f-**P**roxy-**A**utoformalization_), a data generation pipeline that cascades statement autoformalization, proof drafting, and proof search as a proxy autoformalization path.Experiments demonstrate significant improvements: HAR achieves superior performance on FormalMath500 ($15.50\\% \mapsto 43.39\\%$) and MiniF2F-Solving ($21.87\\% \mapsto 55.68\\%$) with lower budget. CoPA shows consistent scalability through expert iteration. Explorations reveal promising directions in formal solution pruning and informal dataset denoising.