神经符号预测器的自动形式化

arXiv:2610.01519v1 公告类型：新提交 摘要：神经符号（NeSy）预测器将先验知识融入神经网络的预测过程，确保输出满足指定约束，因此特别适用于必须遵循领域知识的高风险应用。这一范式的关键瓶颈在于符号约束的获取：将领域知识编码为逻辑公式仍是一个依赖人工且需要大量专家参与的过程。在本研究中，我们探讨通过大语言模型（LLM）进行自动形式化，能够在多大程度上将文本知识系统地转换为可接入 NeSy 预测器的符号知识。为此，我们提出了 auto-nesy-bench，这是一个用于评估约束形式化及其对 NeSy 预测器下游准确率影响的新基准。通过在多个领域开展广泛评估，我们发现，LLM 能够在相当程度上将约束形式化，生成的公式通常与人类专家提供的公式相似。此外，当生成的公式在语法上有效时，它们可以带来高质量的下游预测。代码和基准可在 https://unitn-sml.github.io/auto-nesy-bench/ 获取。