⏶3
形式不确定性语法：自动化推理任务中何时信任大语言模型
发表
由 
Debargha Ganguly 提交
Debargha Ganguly 提交作者: Debargha Ganguly, 
Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, Vipin Chaudhary
Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, Vipin Chaudhary摘要
大语言模型 (LLM) 通过生成形式化规范，在民主化自动化推理方面展现出非凡的潜力。然而，一个根本性的矛盾在于：LLM 是概率性的，而形式化验证则要求确定性的保证。本文通过全面调查 LLM 生成的形式化产物中的故障模式和不确定性量化 (UQ)，来解决这一认识论上的鸿沟。我们对五种前沿 LLM 的系统评估揭示了基于可满足性模理论 (SMT) 的自动形式化对准确性具有领域特定的影响（在逻辑任务上提高 34.8%，在事实任务上降低 44.5%），而像词元概率熵这样的已知 UQ 技术未能识别出这些错误。我们引入了一个概率上下文无关文法 (PCFG) 框架来建模 LLM 输出，从而产生了更精细的不确定性分类。我们发现不确定性信号是任务相关的（例如，逻辑任务的语法熵，AUROC>0.93）。最后，这些信号的轻量级融合实现了选择性验证，在极少弃权的情况下大幅减少了错误（14-100%），将 LLM 驱动的形式化转变为一门可靠的工程学科。
大型语言模型（LLMs）通过生成形式化规范，在普及自动化推理方面展现出非凡的潜力。然而，存在一个根本性的矛盾：LLMs是概率性的，而形式化验证要求确定性保证。本文旨在通过全面调查LLM生成的形式化产物的失败模式和不确定性量化（UQ），来解决这一认知鸿沟。我们对五种前沿LLM的系统评估揭示，基于可满足性模理论（SMT）的自动形式化对准确性存在领域特异性影响（从逻辑任务上的+34.8%到事实任务上的-44.5%），而现有UQ技术，如词元概率的熵，未能识别这些错误。我们引入了一个概率上下文无关文法（PCFG）框架来建模LLM的输出，从而得到了一个更精细的不确定性分类法。我们发现不确定性信号具有任务依赖性（例如，逻辑任务中的语法熵，AUROC>0.93）。最后，这些信号的轻量化融合使得选择性验证成为可能，大幅减少了错误（14-100%），且弃权率极低，从而将LLM驱动的形式化转化为一门可靠的工程学科。