Auto-Formalizing Neuro-Symbolic Predictors
cs.LG, cs.AI
Submitted: 2026-10-01
Updated: 2026-10-01
Code: https://github.com/april-tools/cirkit
Project page: https://unitn-sml.github.io/auto-nesy-bench
License: http://creativecommons.org/licenses/by/4.0/
The gist: Neuro-Symbolic (NeSy) predictors incorporate prior knowledge into the prediction process of neural networks, ensuring that outputs satisfy specified constraints, making them particularly suitable for
Abstract
Neuro-Symbolic (NeSy) predictors incorporate prior knowledge into the prediction process of neural networks, ensuring that outputs satisfy specified constraints, making them particularly suitable for high-stakes applications where compliance with domain knowledge is essential. A key bottleneck in this paradigm is the acquisition of symbolic constraints: encoding domain knowledge into logical formulas remains a manual and expert-intensive process. In this work, we investigate the extent to which auto-formalization via LLMs can systematically translate textual knowledge into symbolic knowledge that can be plugged into NeSy predictors. To this end, we introduce auto-nesy-bench, a new benchmark for evaluating constraint formalization and its impact on downstream accuracy of NeSy predictors. Through an extensive evaluation across several domains, we find that LLMs can formalize constraints to a meaningful extent, generating formulas that are often similar to those provided by human experts. Moreover, when the generated formulas are syntactically valid, they can lead to high-quality downstream predictions. The code and benchmark are available at https://unitn-sml.github.io/auto-nesy-bench/.
Sources
- Holy Grail 2.0: From Natural Language to Constraint Models
- A Neuro-Symbolic Approach for Probabilistic Reasoning on Graph Data
- The Theory and Practice of MAP Inference over Non-Convex Constraints
- DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
- Evaluating Large Language Models Trained on Code
- Program Synthesis with Large Language Models
- DCP-Bench-Open: Evaluating LLMs for Constraint Modelling of Discrete Combinatorial Problems
- Qwen3 Technical Report
- Qwen3-Coder-Next Technical Report
- Gemma 3 Technical Report
- Gemma 4 Technical Report
- Mistral 7B
- DeepSeek-V3 Technical Report
- Phi-4-reasoning Technical Report
- gpt-oss-120b & gpt-oss-20b Model Card
- Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition
- LLM-Assisted Logic Rule Learning: Scaling Human Expertise for Time Series Anomaly Detection
- VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline
- LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving
- The Road to Generalizable Neuro-Symbolic Learning Should be Paved with Foundation Models
Related papers
- Polynomial-Augmented Neural Networks (PANNs) with Weak Orthogonality Constraints for Enhanced Function and PDE Approximation
- AIRL-S: Unifying Reinforcement Learning and Search-Based Test-Time Scaling via Adversarial Inverse Reinforcement Learning
- Transformers as Bayesian In-Context Experimenters: Smoothness-Adaptive Efficient ATE Estimation
- Convergence issues in Relational Concept Analysis based on AOC-posets
- Beliefs Beyond Posteriors: The Predictive Cost of ELBO Binding
- Understanding Diffusion Models via Ratio-Based Function Approximation with SignReLU Networks