自动形式化神经符号预测因子

神经符号 (NeSy) 预测器将先验知识纳入神经网络的预测过程中，确保输出满足指定的约束，使它们特别适合必须遵守领域知识的高风险应用。该范式的一个关键瓶颈是符号约束的获取：将领域知识编码为逻辑公式仍然是一个手动和专家密集的过程。在这项工作中，我们研究了通过大语言模型的自动形式化可以在多大程度上系统地将文本知识转化为可以插入 NeSy 预测器的符号知识。为此，我们引入了 auto-nesy-bench，这是一个用于评估约束形式化及其对 NeSy 预测器下游准确性的影响的新基准。通过跨多个领域的广泛评估，我们发现大语言模型可以在有意义的程度上形式化约束，生成通常与人类专家提供的公式相似的公式。此外，当生成的公式在语法上有效时，它们可以带来高质量的下游预测。代码和基准可在 https://unitn-sml.github.io/auto-nesy-bench/. 获取