auto-nesy-bench: Auto-Formalizing Neuro-Symbolic Predictors

Samuele Bortolotti¹, Weixin Chen², Han Zhao²,
Andrea Passerini¹, Stefano Teso¹, Antonio Vergari³

¹University of Trento, ²University of Illinois Urbana-Champaign, ³University of Edinburgh

Equal contribution Equal supervision

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.

Downloads

Non-redistributable datasets: download_external_datasets.sh (CIFAR-10, CIFAR-100, SUSHI3)

Codebase and data: GitHub

Paper: coming soon

Built on: rsbench (data, code)

Most datasets are shipped with the benchmark archive. CIFAR-10, CIFAR-100 and SUSHI3 cannot be redistributed, so the script above fetches them from their original sources:

# all three datasets into ./data
bash download_external_datasets.sh ./data

# or only some of them
bash download_external_datasets.sh ./data cifar10 sushi

Overview

Why auto-formalization? NeSy predictors guarantee that their predictions satisfy a constraint $𝖪$, but they assume $𝖪$ is handed to them as a well-formed formula. Writing it requires a domain expert. What if an end user wants to deploy a NeSy predictor and no expert is available? We use LLMs as the expert, and translate a textual description of the domain knowledge into a CNF formula.

Our goal. We do not aim to replace domain experts, but to support them. LLM-generated formulas remain interpretable, so a user can inspect and correct them before plugging them into a NeSy predictor. Auto-formalization lowers the barrier to adopting NeSy AI, while keeping a human in control of the knowledge the model relies on.

What does the benchmark provide?

• 18 NeSy tasks adapted from established datasets, ranging from 9 to 102 variables and from 17 to about 130k clauses, spanning arithmetic, puzzles, ranking, path finding, vision, text and autonomous driving.

• Two levels of description: every task comes with a detailed and a non-detailed natural-language description, to measure how much auto-formalization depends on the user’s expertise.

• Grounded variables: every task lists its Boolean variables with their name and meaning, so the benchmark measures constraint formalization rather than symbol identification.

• Annotated data: every task ships input-output annotations, so generated formulas can be evaluated end to end, from constraint extraction to downstream NeSy prediction. Existing SAT and CP formalization benchmarks do not provide this.

• Formula-level metrics based on model counting, which compare the sets of solutions admitted by the generated and ground-truth formulas rather than only their satisfiability.

• Reference ground truth: each ground-truth CNF was compiled with PySAT and checked against a Python oracle, exhaustively whenever the task has at most $2^{20}$ assignments.

We also repurpose two existing benchmarks for auto-formalization: satbench (1,041 satisfiable instances, Wei et al., EMNLP 2025) and dcpbench (85 discrete, non-optimization instances, Michailidis et al., 2026).

Tasks

Every task is adapted from an established dataset. Follow the links in the Source column to see the original datasets, and please cite them (see Source datasets) if you use the corresponding tasks.

Examples

Source datasets

auto-nesy-bench would not exist without the datasets it builds on. If you use a task, please also cite the dataset it comes from.

@article{lecun1998mnist,
  title  = {The {MNIST} database of handwritten digits},
  author = {LeCun, Yann},
  url    = {http://yann.lecun.com/exdb/mnist/},
  year   = {1998}
}

@inproceedings{manhaeve2018deepproblog,
  title     = {{DeepProbLog}: Neural Probabilistic Logic Programming},
  author    = {Manhaeve, Robin and Dumancic, Sebastijan and Kimmig, Angelika and
               Demeester, Thomas and De Raedt, Luc},
  booktitle = {Advances in Neural Information Processing Systems},
  year      = {2018}
}

@inproceedings{augustine2022visual,
  title     = {Visual Sudoku Puzzle Classification: A Suite of Collective Neuro-Symbolic Tasks},
  author    = {Augustine, Eriq and Pryor, Connor and Dickens, Charles and
               Pujara, Jay and Wang, William and Getoor, Lise},
  booktitle = {International Workshop on Neural-Symbolic Learning and Reasoning (NeSy)},
  year      = {2022}
}

@article{xiao2017fashion,
  title   = {{Fashion-MNIST}: a Novel Image Dataset for Benchmarking Machine Learning Algorithms},
  author  = {Xiao, Han and Rasul, Kashif and Vollgraf, Roland},
  journal = {arXiv preprint arXiv:1708.07747},
  year    = {2017}
}

@techreport{krizhevsky2009learning,
  title       = {Learning Multiple Layers of Features from Tiny Images},
  author      = {Krizhevsky, Alex and Hinton, Geoffrey},
  institution = {University of Toronto},
  year        = {2009}
}

@inproceedings{xu2020explainable,
  title     = {Explainable Object-Induced Action Decision for Autonomous Vehicles},
  author    = {Xu, Yiran and Yang, Xiaoyin and Gong, Lihang and Lin, Hsuan-Chu and
               Wu, Tz-Ying and Li, Yunsheng and Vasconcelos, Nuno},
  booktitle = {IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR)},
  year      = {2020}
}

@article{giunchiglia2023roadr,
  title   = {{ROAD-R}: The Autonomous Driving Dataset with Logical Requirements},
  author  = {Giunchiglia, Eleonora and Stoian, Mihaela C{\u{a}}t{\u{a}}lina and
             Khan, Salman and Cuzzolin, Fabio and Lukasiewicz, Thomas},
  journal = {Machine Learning},
  volume  = {112},
  number  = {9},
  pages   = {3261--3291},
  year    = {2023}
}

@inproceedings{kamishima2003nantonac,
  title     = {Nantonac Collaborative Filtering: Recommendation Based on Order Responses},
  author    = {Kamishima, Toshihiro},
  booktitle = {Proceedings of the Ninth ACM SIGKDD International Conference on
               Knowledge Discovery and Data Mining},
  pages     = {583--588},
  year      = {2003}
}

@inproceedings{abraham2022cebab,
  title     = {{CEBaB}: Estimating the Causal Effects of Real-World Concepts on {NLP} Model Behavior},
  author    = {Abraham, Eldar D and D'Oosterlinck, Karel and Feder, Amir and Gat, Yair and
               Geiger, Atticus and Potts, Christopher and Reichart, Roi and Wu, Zhengxuan},
  booktitle = {Advances in Neural Information Processing Systems},
  volume    = {35},
  pages     = {17582--17596},
  year      = {2022}
}

@inproceedings{cohen2022torchxrayvision,
  title     = {{TorchXRayVision}: A library of chest {X}-ray datasets and models},
  author    = {Cohen, Joseph Paul and Viviano, Joseph D. and Bertin, Paul and
               Morrison, Paul and Torabian, Parsa and Guarrera, Matteo and
               Lungren, Matthew P and Chaudhari, Akshay and Brooks, Rupert and
               Hashir, Mohammad and Bertrand, Hadrien},
  booktitle = {Proceedings of the 5th International Conference on Medical Imaging with Deep Learning},
  series    = {Proceedings of Machine Learning Research},
  volume    = {172},
  pages     = {231--249},
  year      = {2022}
}

@inproceedings{vlastelica2020differentiation,
  title     = {Differentiation of Blackbox Combinatorial Solvers},
  author    = {Vlastelica Pogan{\v{c}}i{\'c}, Marin and Paulus, Anselm and Musil, Vit and
               Martius, Georg and Rolinek, Michal},
  booktitle = {International Conference on Learning Representations},
  year      = {2020}
}

@article{muller2021kandinsky,
  title   = {Kandinsky Patterns},
  author  = {M{\"u}ller, Heimo and Holzinger, Andreas},
  journal = {Artificial Intelligence},
  volume  = {300},
  pages   = {103546},
  year    = {2021}
}

@inproceedings{johnson2017clevr,
  title     = {{CLEVR}: A Diagnostic Dataset for Compositional Language and
               Elementary Visual Reasoning},
  author    = {Johnson, Justin and Hariharan, Bharath and van der Maaten, Laurens and
               Fei-Fei, Li and Zitnick, C Lawrence and Girshick, Ross},
  booktitle = {IEEE Conference on Computer Vision and Pattern Recognition (CVPR)},
  year      = {2017}
}

Detailed vs. non-detailed descriptions

Each task description comes in two variants. The detailed variant spells out every rule and lists the background facts that should not be encoded; the non-detailed variant describes the same task in ordinary prose and leaves more of the rule decomposition to the model. Two authors wrote both variants independently, one acting as an expert and one as a non-expert, and then reconciled them clause by clause. Only the constraint description changes between the two conditions: the prompt template and variable list are byte-identical. For example, for sushi:

[DETAILED]
- Each sushi item must be assigned to exactly one preference rank.
- Every rank must be assigned to exactly one sushi item.
- Each sushi item cannot be assigned to more than one rank.
- No two sushi items can share the same rank.

[NOT DETAILED]
- Encode a valid permutation matrix representing a complete ranking of the
  four sushi items.

Evaluation

What are NeSy predictors?

NeSy predictors are classifiers designed for reliability. Given an input $𝒙\in {ℝ}^n$, they predict a (multi-)label $𝒚\in \{0,1{\}}^m$ while leveraging prior knowledge $𝖪$, usually structural or safety requirements over the outputs. The model produces a predictive distribution $p_{\theta }(𝒚\mid 𝒙;𝖪)$ that assigns lower, or even provably zero, probability to outputs that violate $𝖪$:

For example, a self-driving car deciding whether to move forward from an image of the road can be given the constraint $𝖪:(\mathtt{\text{𝚐𝚛𝚎𝚎𝚗}}\wedge \mathtt{\text{𝚌𝚕𝚎𝚊𝚛}})\Rightarrow \mathtt{\text{𝚏𝚘𝚛𝚠𝚊𝚛𝚍}}$. The neural network alone may put mass on $\mathtt{\text{𝚐𝚛𝚎𝚎𝚗}}=1,\mathtt{\text{𝚌𝚕𝚎𝚊𝚛}}=1,\mathtt{\text{𝚏𝚘𝚛𝚠𝚊𝚛𝚍}}=0$; a NeSy predictor rules that combination out and renormalizes over the assignments that satisfy $𝖪$. This only works if $𝖪$ is correct, which is why we evaluate both the generated formulas and the predictors built on them.

Formula quality

Existing benchmarks check whether a generated formula has the right satisfiability status. A NeSy predictor needs more than that: it needs to know which assignments the formula admits, because it assigns probability mass only to those. We therefore compare the generated formula $\hat{\varphi }$ with the ground truth ${\varphi }^{\ast }$ over $N$ variables through model counting ($\mathrm{MC}$):

Counts are exact for tasks with at most 20 variables and use ApproxMC otherwise. Auxiliary (Tseitin) variables are projected out before any negation or conjunction. From these counts we derive

Recall matters most: a formula that wrongly excludes a valid assignment makes that output impossible to predict. We also report the syntax error rate over the $n$ generated formulas, after self-verification:

Downstream NeSy predictors

We train each predictor with the generated formula and compare it with the same backbone trained on the ground-truth formula, using F1, precision, recall and accuracy on a held-out test set, plus three metrics tailored to our setting.

Consistency (Con): the fraction of the $N$ test predictions that satisfy the ground-truth formula,

A consistency below 1 means that some predictions violate the constraints, which can be harmful in the downstream application.

Formula relationship (Rel): we test the two subset relations exactly,

and assign each generated formula one of four relations:

Model-count ratio (MC-R): how many more (or fewer) assignments the generated formula admits,

For example, a permissive formula with MC-R = 1.75 admits 75% more assignments than the ground truth.

Evaluation pipeline

In the paper, we use auto-nesy-bench to evaluate an end-to-end pipeline: an LLM formalizes the constraint, and the resulting formula is plugged into a NeSy predictor used for learning and inference (see the figure at the top of the page).

Auto-formalization

Prompting. Each prompt frames the LLM as an expert in SAT solving and constraint modeling, gives the grounded variables and the constraint description, and asks for the formula inside a <cnf>...</cnf> block in one of five formats: raw DIMACS, natural-language Boolean operators (NAT), or Python programs using PySAT, CPMpy or SymPy. The LLM may introduce auxiliary variables, provided they are defined in terms of the given ones.

Self-verification. When the output has a syntax error, the LLM receives the erroneous formula and the error message, and answers either [[OK]] or [[FIXED]] followed by a corrected formula, for up to five rounds. Formatting issues that need no reasoning, such as a wrong DIMACS header or a missing Python import, are fixed automatically.

Compilation. Every output is converted to DIMACS and compiled into a sentential decision diagram with PySDD. Auxiliary variables are existentially quantified, so the circuit is defined over the same variables as the ground truth.

NeSy predictors: SPL and SL

Semantic probabilistic layer (SPL, hard constraint). SPL sits on top of a neural network and combines its unconstrained distribution $q_{\theta }(𝒚\mid 𝒙)$ with a constraint circuit $c_{𝖪}\left(𝒚\right)$, which is non-zero only if $𝒚\models 𝖪$:

The partition function $Z_{𝒙}$ is computed exactly on the circuit. SPL is trained by maximum likelihood, $ℒ=-𝔼\left[\log p_{\theta }(𝒚\mid 𝒙;𝖪)\right]$, and predicts $\widehat{𝒚}={\mathrm{argmax}}_{𝒚}{p}_{\theta }(𝒚\mid 𝒙;𝖪)$, so every prediction satisfies $𝖪$ by construction. We implement it with cirkit.

Semantic loss (SL, soft constraint). SL keeps a standard classifier with independent outputs $p_{\theta }(Y_i\mid 𝒙)$ and penalizes the probability mass it places outside $𝖪$:

The sum is the weighted model count of $𝖪$, computed on the same circuit with KLay; we use $\lambda =1$. At test time, SL predicts $\widehat{𝒚}={\mathrm{argmax}}_{𝒚}{p}_{\theta }(𝒚\mid 𝒙)$, with no guarantee of consistency.

The formula therefore matters in different ways: in SPL an incorrect formula rules out valid predictions or allows invalid ones, while in SL it only biases training.

Evaluated models

We evaluate eleven open-weight LLMs, from 8.2B to 117B parameters: qwen3-8b, qwen3-32b, qwen3-coder-next, mistral-nemo, phi4-reasoning-plus, gemma3-27b, gemma4-31b, olmo3-32b-think, deepseek-r1-llama-70b, gpt-oss-20b and gpt-oss-120b. Each model is run with zero-shot (ZS) and zero-shot chain-of-thought (ZS-CoT) prompts, across the five output formats, with a budget of five self-verification steps. For the downstream experiments, we train SPL and SL with the formulas that gpt-oss-120b, olmo3-32b-think and qwen3-8b generate with CPMpy and a detailed ZS-CoT prompt, over five seeds.

Key findings

• LLMs can formalize NeSy constraints, but not perfectly. Averaged over formats and prompts, gpt-oss-120b reaches an F1 of 0.786 and gemma4-31b 0.706 on auto-nesy-bench. With their best configuration (ZS-CoT and CPMpy), both exceed 0.98 F1. Weaker models such as gemma3-27b and mistral-nemo fail to produce parsable formulas more than half of the time.

• Detail matters. Detailed descriptions raise average F1 from 0.330 to 0.455, and chain-of-thought improves F1 on all three benchmarks.

• Code beats raw CNF. CPMpy (0.575 F1) and SymPy (0.549) outperform direct DIMACS (0.364) and NAT (0.331) generation on auto-nesy-bench. On satbench, NAT is best.

• Generated formulas work downstream. With detailed prompts, SPL models trained on LLM-generated formulas differ from those trained on expert formulas by less than 0.03 F1 on average, and most formulas are exactly equivalent to the ground truth. Overly strict formulas are the most harmful, while permissive ones have little effect.

• SL is more forgiving than SPL. Used as a soft constraint, an imperfect formula does not prevent training, although formulas that conflict with the ground truth still lower consistency.

• auto-nesy-bench sits between existing benchmarks. The best models nearly solve satbench (0.963 F1), while dcpbench remains hard (0.324). auto-nesy-bench is challenging but tractable.

Results on auto-nesy-bench. Each row is averaged over models and over the factors it does not fix; for example, prompting rows average over output formats. Output-format rows use only the detailed description. Mean ± standard deviation; the best value in each group is in bold.

Results per LLM on auto-nesy-bench. Each row is averaged over the five output formats and both prompting strategies, using the detailed description. Models are ordered by size. Best value in bold, second best underlined.

License

Code: distributed under the BSD 3-Clause license.

Data: labels, CNF targets and any bundled images or features are distributed under the CC BY-NC-SA 4.0 license. This is the most restrictive license among the bundled datasets, inherited from ROAD-R; all other bundled datasets use licenses that are equally or more permissive.

Datasets not redistributed. SUSHI3 must be downloaded from Kamishima’s archive, whose license explicitly forbids redistribution. CIFAR-10 and CIFAR-100 have no explicit license or redistribution grant, so they are downloaded from the original page (or via torchvision). The download_external_datasets.sh script does both. By running it, you agree to each dataset’s terms of use.

Citation

If you use auto-nesy-bench, please cite:

@misc{bortolotti2026autoformalizing,
  title={Auto-Formalizing Neuro-Symbolic Predictors},
  author={Samuele Bortolotti and Weixin Chen and Han Zhao and Andrea Passerini and Stefano Teso and Antonio Vergari},
  year={2026},
  eprint={2610.01519},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2610.01519},
}

auto-nesy-bench extends rsbench:

@inproceedings{bortolotti2024benchmark,
  title     = {A Neuro-Symbolic Benchmark Suite for Concept Quality and Reasoning Shortcuts},
  author    = {Bortolotti, Samuele and Marconato, Emanuele and Carraro, Tommaso and
               Morettin, Paolo and van Krieken, Emile and Vergari, Antonio and
               Teso, Stefano and Passerini, Andrea},
  booktitle = {Advances in Neural Information Processing Systems},
  volume    = {37},
  pages     = {115861--115905},
  year      = {2024}
}

Acknowledgments

Funded by the European Union, Grant Agreement no. 101120763 (TANGO). Views and opinions expressed are those of the author(s) only and do not necessarily reflect those of the European Union or the European Health and Digital Executive Agency (HaDEA); neither can be held responsible for them. Antonio Vergari is supported by the “UNREAL: Unified Reasoning Layer for Trustworthy ML” project (EP/Y023838/1), selected by the ERC and funded by UKRI EPSRC. Stefano Teso was partially supported by the Flemish research foundation (FWO) project “Neurosymbolic AI for Constraint Learning” (G047124N). Weixin Chen and Han Zhao are partially supported by an NSF grant #2504555.