LLM2D
面向实用的第一order模型计数
Towards Practical First-Order Model Counting
作者: Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas, Kuldeep S. Meel
发布日期: 2/19/2025
arXiv ID: oai:arXiv.org:2502.12278v1

摘要

arXiv:2502.12278v1 公告类型: cross 摘要: 一阶模型计数(FOMC)是计算一阶逻辑句子的模型数量的问题。由于提升推理技术依赖于FOMC的各种变体,因此在过去十年中,理论工作者和实践者都关注于设计可扩展的FOMC方法。最近,提出了一种基于一阶知识编译的新方法。该方法称为Crane,它不仅提供了最终计数,还生成了(可能递归的)函数的定义,这些函数可以接受不同的参数来计算任何领域大小的模型计数。然而,这种方法并非完全自动化,因为它需要手动评估构建的函数。本文的主要贡献是一种完全自动化的编译算法,称为Gantry,该算法将函数定义转换为配备了任意精度算术的C++代码。这些添加使得新的FOMC算法能够扩展到比当前最先进的技术大50多万倍的领域大小,实验结果证明了这一点。