# Auto-Formalizing Neuro-Symbolic Predictors

arXiv: https://arxiv.org/abs/2610.01519 · HTML: https://mlsanity.com/paper/2610.01519/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 26 of its 136 references that are in the map.
- First posted on arXiv 1 Oct 2026.

## Builds on (most cited first, 26 of 26)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [Gemma 3 Technical Report](https://mlsanity.com/paper/2503.19786/) (2025)
- [gpt-oss-120b & gpt-oss-20b Model Card](https://mlsanity.com/paper/2508.10925/) (2025)
- [DeepSeek-V3 Technical Report](https://mlsanity.com/paper/2412.19437/) (2024)
- [Gemma 4 Technical Report](https://mlsanity.com/paper/2607.02770/) (2026)
- [Phi-4-reasoning Technical Report](https://mlsanity.com/paper/2504.21318/) (2025)
- [Tree-Structured Parzen Estimator: Understanding Its Algorithm Components and Their Roles for Better Empirical Performance](https://mlsanity.com/paper/2304.11127/) (2023)
- [Qwen3-Coder-Next Technical Report](https://mlsanity.com/paper/2603.00729/) (2026)
- [Holy Grail 2.0: From Natural Language to Constraint Models](https://mlsanity.com/paper/2308.01589/) (2023)
- [Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition](https://mlsanity.com/paper/2504.03930/) (2025)
- [The Role of Foundation Models in Neuro-Symbolic Learning and Reasoning](https://mlsanity.com/paper/2402.01889/) (2024)
- [To Ask or Not to Ask: Learning to Require Human Feedback](https://mlsanity.com/paper/2510.08314/) (2025)
- [The DeepLog Neurosymbolic Machine](https://mlsanity.com/paper/2508.13697/) (2025)
- [The Road to Generalizable Neuro-Symbolic Learning Should be Paved with Foundation Models](https://mlsanity.com/paper/2505.24874/) (2025)
- [DCP-Bench-Open: Evaluating LLMs for Constraint Modelling of Discrete Combinatorial Problems](https://mlsanity.com/paper/2506.06052/) (2025)
- [A Neuro-Symbolic Approach for Probabilistic Reasoning on Graph Data](https://mlsanity.com/paper/2507.21873/) (2025)
- [LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving](https://mlsanity.com/paper/2512.04374/) (2025)
- [LLM-Assisted Logic Rule Learning: Scaling Human Expertise for Time Series Anomaly Detection](https://mlsanity.com/paper/2601.19255/) (2026)
- [VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline](https://mlsanity.com/paper/2604.10341/) (2026)
- [Concise and Logically Consistent Conformal Sets for Neuro-Symbolic Concept-Based Models](https://mlsanity.com/paper/2605.18202/) (2026)
- [sLTN: Structural Logic Tensor Networks](https://mlsanity.com/paper/2608.11136/) (2026)

## Abstract (arXiv)

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/.