让大模型生成逻辑程序，实现可验证的推理与高效执行
On LLM-generated Logic Programs and their Inference Execution Methods
- 将大模型输出转为命题逻辑、关系三元组等逻辑程序
- 通过向量库软匹配事实，支持大规模逻辑推理
- 用GPU加速最小模型计算，提升推理效率
大语言模型（LLMs）在海量数据上训练，高度压缩了人类积累的大量知识。本文研究如何将这些知识以命题霍恩子句、双霍恩子句、关系三元组和确定性语法等形式提取为逻辑程序。将知识显式表达为逻辑程序，可支持严谨的推理方法，用于验证模型输出是否符合预期用途，并拓展其推理能力。本文提出新的执行方法，包括将可消去事实与存储在向量数据库中的大模型生成内容进行软统一匹配，以及利用GPU加速最小模型计算，从而支持大规模逻辑程序的推理。该方法提升了推理的准确性与效率。
原文摘要 · Abstract (English)
Large Language Models (LLMs) trained on petabytes of data are highly compressed repositories of a significant proportion of the knowledge accumulated and distilled so far. In this paper we study techniques to elicit this knowledge in the form of several classes of logic programs, including propositional Horn clauses, Dual Horn clauses, relational triplets and Definite Clause Grammars. Exposing this knowledge as logic programs enables sound reasoning methods that can verify alignment of LLM outputs to their intended uses and extend their inference capabilities. We study new execution methods for the generated programs, including soft-unification of abducible facts against LLM-generated content stored in a vector database as well as GPU-based acceleration of minimal model computation that supports inference with large LLM-generated programs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。