发表机构
University of Trento; University of Illinois Urbana-Champaign; University of Edinburgh（特伦托大学; 伊利诺伊大学厄巴纳-香槟分校; 爱丁堡大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究提出auto-nesy-bench基准，利用大语言模型自动将文本知识形式化为符号约束，集成到神经符号预测器中，实验表明生成公式接近专家水平且能提升下游预测准确性。
AI 中文摘要
神经符号（NeSy）预测器将先验知识融入神经网络的预测过程中，确保输出满足特定约束，使其特别适用于必须符合领域知识的高风险应用。该范式的一个关键瓶颈在于符号约束的获取：将领域知识编码为逻辑公式仍然是一个人工且高度依赖专家的过程。在本工作中，我们研究了通过大语言模型（LLM）进行自动形式化能在多大程度上系统地将文本知识转化为可嵌入NeSy预测器的符号知识。为此，我们引入了auto-nesy-bench，一个新的基准，用于评估约束形式化及其对NeSy预测器下游准确性的影响。通过在多个领域的大量评估，我们发现LLM能够在有意义的程度上形式化约束，生成的公式通常与人类专家提供的公式相似。此外，当生成的公式在语法上有效时，它们可以带来高质量的下游预测。代码和基准可在该https URL获取。
英文摘要
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/.
