NF-Bridge: Faithfully Bridging Natural and Formal Languages for Mathematical Reasoning

Natural-language and formal-language reasoning and proving constitute two important paths for advancing mathematical theory: the former supports flexible mathematical expression, while the latter provides rigorous machine verification. However, faithfully converting between these two proof forms and effectively combining their respective strengths remains a central challenge. To address this problem, we propose NF-Bridge, a faithfulness-centered framework that connects natural-language mathematical reasoning with formal verification. NF-Bridge first converts a candidate natural-language solution into a semantic proposition DAG, which explicitly represents answer-relevant mathematical assertions and their dependency structure, while abstracting away rhetorical and repetitive content without discarding key mathematical commitments. The entire DAG is then formalized into Lean representations. Compilation-based verification and semantic-fidelity evaluation are subsequently used to assess, respectively, the syntactic and type-level validity of the formalization and its consistency with the original natural-language argument. We further demonstrate that NF-Bridge not only supports faithful autoformalization of natural-language proofs, but also enables the construction of formal-verification-grounded reward signals for improving mathematical reasoning. Across AIME24, AIME25, MATH-500, and BRUMO25, the verifier-based reward derived from NF-Bridge outperforms multiple learned reward-model baselines. As additional evaluations of its underlying proof-autoformalization capability, NF-Bridge also achieves strong results on ProofFlowBench and RobustPABench.