---
title: "Verifiable PDE Reasoning and Modeling with Neurosymbolics"
authors:
  - "Wuyang Chen"
doi: "10.24963/ijcai.2026/903"
url: "https://ijcai.org/proceedings/2026/903"
pdf: "https://ijcai.org/proceedings/2026/0903.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "8144-8149"
track: "Early Career Spotlight"
keywords:
  - "AI: Agent-based and Multi-agent Systems"
  - "AI: Machine Learning"
  - "AI: Multidisciplinary Topics and Applications"
  - "AI: Knowledge Representation and Reasoning"
---

# Verifiable PDE Reasoning and Modeling with Neurosymbolics

Wuyang Chen

*Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence*, pages 8144-8149. DOI: [10.24963/ijcai.2026/903](https://doi.org/10.24963/ijcai.2026/903)

## Abstract

Recent progress in Large Language Models (LLMs) has transformed text and code generation, yet models still falter on Partial Differential Equations (PDEs) where correctness, constraints, and physical consequences are critical. We explore how formal LLM reasoning can advance symbolic PDE modeling. First, our PDE-Controller formalizes informal PDEs, synthesizes solver-ready code, and plans subgoals to tackle nonconvex control via interactions with external solvers. Second, our Lean Finder accelerates PDE formalization via a semantics-aware search engine for Lean/Mathlib that retrieves relevant theorems, outperforming GPT models and gaining significant traction in the AI-for-math community. Through these efforts, we aim to design a semantics-first LLM that autoformalizes informal PDE problems into machine-checked specifications and synthesizes solver-ready code. This closes the loop between formal analysis and LLM reasoning, ultimately surpassing human heuristics across PDEs.