🚀 Excited to share our paper: "A Survey on Deep Learning for Theorem Proving"! Dive into our extensive review of DL tasks, methods, datasets, and evaluations in #TheoremProving! Paper: arxiv.org/abs/2404.09939 Github: github.com/zhaoyu-li/DL4TP

Can AI transform human mathematics into formal theorems and proofs that machines can verify? This process, known as autoformalization, is a key step towards AI mathematicians. We introduce a neuro-symbolic framework for autoformalization, focusing on Euclidean geometry and

🚀 Exciting News for Developers! Introducing 🍎APPL: A Prompt Programming Language that seamlessly blends Natural Language Prompts with Python programs. Boost your LLM workflow with APPL now! #AI #Coding #LLM #Python #APPL [1/6] 🔥 Start here: appl-team.github.io/appl/#quick-st… 📚

Our survey paper on neural theorem proving has been accepted at Conference on Language Modeling! It's great to see the growing interest in this field, with many new papers appearing on arXiv recently. We will include the latest methods and advancements in our revision. Stay tuned! #COLM #COLM2024

Humans can learn to reason in an "unfamiliar" world, like new games. How far are LLMs from this? Check out our recent work @NeurIPS2024 D&B Track: "LogiCity: Advancing Neuro-Symbolic AI with Abstract Urban Simulation". Page: jaraxxus-me.github.io/LogiCity/

Mitigating racial bias from LLMs is a lot easier than removing it from humans! Can’t believe this happened at the best AI conference NeurIPS Conference We have ethical reviews for authors, but missed it for invited speakers? 😡

🚀 Excited to share our position paper: "Formal Mathematical Reasoning: A New Frontier in AI"! 🔗 arxiv.org/abs/2412.16075 LLMs like o1 & o3 have tackled hard math problems by scaling test-time compute. What's next for AI4Math? We advocate for formal mathematical reasoning,

🚀 Excited to share our #ICLR2025 paper: "Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning"! 📄 Paper: arxiv.org/pdf/2502.13834 LLMs like R1 & o3 excel at solving complex, calculation-based math problems. However, when it comes to proving inequalities in

Come join our AI for Math & Theorem Proving social at #ICLR2025! Looking forward to talking with everyone interested in LLMs for reasoning!

LLMs solving math benchmarks with verifiable answers like AIME? ✅ LLMs solving math proofs? ❌ Still an open problem. RL works great for final-answer problems, but proofs are different: - Often no single checkable answer - Correct answers can hide flawed reasoning The key