Auto-Formalizing Neuro-Symbolic Predictors
Neuro-symbolic predictors require hand-crafted logical constraints, which limits adoption by practitioners without formal-methods expertise. This paper asks whether LLMs can translate natural language into propositional constraints that plug into NeSy predictors, and introduces auto-nesy-bench—an 18-task benchmark that measures both formalization fidelity and downstream accuracy. The core finding is that frontier LLMs can generate formulas approaching expert quality, and when the formulas are syntactically valid they often preserve downstream predictor performance, suggesting a plausible path toward making reliable NeSy AI more accessible.
The paper makes a timely contribution by connecting constraint auto-formalization to the downstream behavior of NeSy predictors, a link largely missing from prior SAT and CP benchmarks. The evaluation is principled: the authors ground variables explicitly to isolate formalization, use exact or approximate model counting to compare full solution sets, and test generated constraints inside a semantic probabilistic layer and via semantic loss. Best-performing models such as gpt-oss-120b achieve strong F1 scores (0.963 on satbench and 0.786 on auto-nesy-bench), and downstream SPL accuracy drops by less than 0.03 F1 on average when using LLM-generated formulas. Nevertheless, the picture is qualified by high syntax-error rates for smaller models, frequent task failures for mid-sized LLMs, and a limited 18-task benchmark that tempers broad claims about generalizability.
The benchmark design and the model-counting evaluation metric are the paper’s strongest assets. Unlike prior work that checks only satisfiability, the authors compute true positives via exact or approximate model counting over the full set of assignments and derive precision, recall, and a fine-grained formula-relationship taxonomy (equal, permissive, strict, incomparable). This directly measures whether a generated constraint incorrectly forbids valid outputs—a critical failure mode for predictors like SPL that allocate zero mass to excluded assignments. The downstream experiments are also valuable: they show that exact formula equivalence is not necessary, as permissive formulas can still yield accurate in-distribution predictions because the neural network learns to down-weight invalid combinations.
The main flaw is limited scale and over-claiming practicability. Auto-nesy-bench contains only 18 tasks, and even within this small set mid-sized and small LLMs fail frequently—olmo3-32b-think fails on 6 of 18 tasks and qwen3-8b on 7 of 18, while only gpt-oss-120b succeeds everywhere. By providing fully grounded variables, the authors sidestep symbol grounding, a core bottleneck in real-world deployment.
Furthermore, the positive downstream results are conditional on syntactic validity and successful compilation, yet many models exhibit syntax error rates above 30%. On dcpbench the best F1 is only 0.324, indicating poor generalization outside the authors’ curated NeSy problems. The conclusion that LLMs can act as domain experts is therefore only tenable for frontier models in narrow, pre-structured settings.
The central evidence—that LLM formulas can substitute for expert-written constraints in SPL—is well-supported for top-tier models on the authors’ benchmark, but comparisons are uneven across datasets. Near-ceiling performance on satbench (F1 0.963) contrasts with weak dcpbench results, and the paper does not deeply explain why code-based formats excel on auto-nesy-bench and dcpbench while natural language dominates satbench. The formula-level metrics are a clear advance over prior SAT/CP benchmarks that only verify satisfiability, but the downstream comparison lacks a strong unconstrained-neural-network ablation, which would clarify whether the reported small F1 deltas are meaningful. Related work coverage is adequate, though the novelty of the end-to-end fidelity metrics relative to prior feasibility checks could be sharpened.
Reproducibility is facilitated by publicly released benchmark code and data via the project website and GitHub, and the authors report downstream results averaged over multiple seeds. However, critical training hyperparameters for SPL and SL are deferred to Appendix H and are not detailed in the main text, and the paper omits LLM sampling parameters such as temperature or top-p. The pipeline depends on a specialized software stack—PySDD, cirkit, KLay, and ApproxMC—and knowledge-compilation failures are common enough that the authors report run failures as a separate category, which may complicate independent reproduction on different hardware or library versions.
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/.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.