形式不确定性的语法：在自动化推理任务中何时信任 LLM
计算与语言
2025-05-27 v1 人工智能
计算机科学中的逻辑
软件工程
摘要
大型语言模型 通过生成形式规约，在普及自动化推理方面展现出巨大潜力。然而，存在一个根本性的矛盾：LLM 是概率性的，而形式验证要求确定性的保证。本文通过全面研究 LLM 生成的形式产物中的失败模式和不确定性量化 (UQ)，解决了这一认识论上的差距。我们对五个前沿 LLM 的系统评估揭示了基于可满足性模理论 的自动形式化对准确率的领域特定影响（从逻辑任务上的 +34.8% 到事实任务上的 -44.5%），而已知的 UQ 技术（如 token 概率的熵）无法识别这些错误。我们引入了概率上下文无关文法 (PCFG) 框架来对 LLM 输出进行建模，产生了精细的不确定性分类体系。我们发现不确定性信号具有任务依赖性（例如，逻辑任务的语法熵，AUROC>0.93）。最后，这些信号的轻量级融合实现了选择性验证，在极少弃权的情况下大幅减少了错误 (14-100%)，将 LLM 驱动的形式化转化为可靠的工程学科。
引用
@article{arxiv.2505.20047,
title = {Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks},
author = {Debargha Ganguly and Vikash Singh and Sreehari Sankar and Biyao Zhang and Xuecen Zhang and Srinivasan Iyengar and Xiaotian Han and Amit Sharma and Shivkumar Kalyanaraman and Vipin Chaudhary},
journal= {arXiv preprint arXiv:2505.20047},
year = {2025}
}