analiza aiqbench
This research demonstrates how Large Language Models can automate the translation of textual domain knowledge into symbolic constraints, effectively addressing a major bottleneck in Neuro-Symbolic AI systems. By validating these auto-generated formulas against human expert benchmarks, the study confirms that LLMs can produce syntactically valid logic that significantly improves downstream prediction accuracy without manual intervention. The release of the `auto-nesy-bench` benchmark provides a crucial tool for evaluating constraint formalization across diverse domains.
Auto-Formalizing Neuro-Symbolic Predictors
arXiv:2610.01519v1 Announce Type: cross 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/.
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 this https URL.
Machine Learning (cs.LG); Artificial Intelligence (cs.AI)
arXiv:2610.01519 [cs.LG]
(or arXiv:2610.01519v1 [cs.LG] for this version)
https://doi.org/10.48550/arXiv.2610.01519 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Text integral sub licența deschisă a publicației · 258 cuvinte
Subiecte conexe
LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers
arXiv · 22 sept. 2026
Towards Probabilistic Question Answering Over Tabular Data
arXiv · 6 oct. 2026
NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
arXiv · 1 sept. 2026
Have You Been Convinced? A Neuro-symbolic Argumentation Reasoning Approach to Detecting Persuasiveness in ChangeMyView Discussions
arXiv · 15 oct. 2026