Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore neuro-symbolic approaches that enhance Large Language Model reasoning capabilities by integrating automated reasoning tools for natural language to formal language tasks. Learn about corrective feedback loop methods that improve LLM performance through logical feedback from compilers, SAT/SMT solvers, and proof assistants during fine-tuning. Discover CoTran, a system that leverages compiler and symbolic execution feedback to ensure syntactic correctness and functional equivalence when translating Java programs to Python. Examine Reinforcement Learning via Symbolic Feedback (RLSF), a framework that generates C++ programs from natural language pseudo-code using token-level symbolic feedback through poly-sized certificates for error identification. Delve into AI for Mathematics applications, focusing on natural language and formal language joint embedding for auto-formalization and automated proof synthesis in Lean. Understand the limitations of existing methods that treat theorem translation and proof generation separately, and explore ProofBridge, a unified framework that translates entire natural language theorems and proofs into Lean 4. Master the joint embedding model that aligns natural language and formal language theorem-proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant formal language examples to guide translation. Analyze how ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean's type checker and LLM feedback to improve semantic and type correctness, demonstrating significant enhancements in LLM reasoning and formalization capabilities across both code and mathematics domains.
