There is a growing trend of leveraging Large Language Models (LLMs) for natural language to formal language (NL-to-FL) tasks, such as code and proof generation. As these tasks demand syntactic precision and logical consistency, there is increasing recognition that tightly integrating LLMs with automated reasoning tools (such as compilers, SAT/SMT solvers, symbolic execution engines, and proof assistants) can substantially enhance their effectiveness.

In the first part of the talk, we briefly explore corrective feedback loop–based neuro-symbolic approaches that improve LLM reasoning by incorporating logical feedback from automated reasoning tools during fine-tuning. We demonstrate their effectiveness in AI for Software Engineering tasks such as code translation and generation. Our work, CoTran, leverages compiler and symbolic execution feedback to ensure syntactic correctness and functional equivalence when translating Java programs to Python. We also present Reinforcement Learning via Symbolic Feedback (RLSF), a framework that generates C++ programs from NL pseudo-code using token-level symbolic feedback through poly-sized certificates identifying errors.

In the second part, we build on these neuro-symbolic ideas and explore their natural extension to AI for Mathematics, focusing on NL/FL joint embedding for auto-formalization and automated proof synthesis in Lean. Existing methods often treat theorem translation and proof generation separately, limiting true proof auto-formalization; even recent systems like AlphaProof require manual NL-to-FL translation of theorems before proof synthesis. We present ProofBridge, a unified framework that translates entire NL theorems and proofs into Lean 4. At its core is a joint embedding model aligning NL and FL theorem–proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant FL examples to guide translation. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean's type checker and LLM feedback to improve semantic and type correctness.

Overall, this talk demonstrates how neuro-symbolic methods can significantly enhance LLM reasoning and formalization capabilities in both code and mathematics.