Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

📄 arXiv: 2505.20047v1 📥 PDF

作者: Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, Vipin Chaudhary

分类: cs.CL, cs.AI, cs.LO, cs.SE

发布日期: 2025-05-26

💡 一句话要点

提出基于PCFG的LLM不确定性量化框架，提升自动推理任务可靠性

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 自动推理 形式化验证 不确定性量化 概率上下文无关文法

📋 核心要点

  1. 现有LLM在自动推理任务中生成形式化规范时，缺乏对自身不确定性的有效量化，导致结果不可靠。
  2. 提出基于概率上下文无关文法(PCFG)的框架，对LLM输出进行建模，从而量化不同任务中的不确定性。
  3. 实验表明，该方法能有效识别LLM生成的错误，并通过选择性验证显著提升自动推理的可靠性。

📝 摘要（中文）

大型语言模型(LLM)在生成形式化规范方面展现出巨大的潜力，有望普及自动推理。然而，LLM的概率性本质与形式验证对确定性保证的需求之间存在根本矛盾。本文通过全面研究LLM生成的形式化制品中的失效模式和不确定性量化(UQ)，旨在解决这一认知差距。对五个前沿LLM的系统评估表明，基于可满足性模理论(SMT)的自动形式化对准确率的影响具有领域特定性（逻辑任务上+34.8%，事实任务上-44.5%），且已知的UQ技术（如token概率的熵）无法识别这些错误。本文引入概率上下文无关文法(PCFG)框架来建模LLM的输出，从而产生更精细的不确定性分类。研究发现，不确定性信号具有任务依赖性（例如，逻辑任务的文法熵，AUROC>0.93）。最后，这些信号的轻量级融合能够实现选择性验证，大幅减少错误（14-100%），同时保持最小的拒绝率，从而将LLM驱动的形式化转变为可靠的工程学科。

🔬 方法详解

问题定义：论文旨在解决LLM在自动推理任务中生成形式化规范时，由于其概率性本质导致结果不确定，进而影响自动推理可靠性的问题。现有方法，如直接使用token概率的熵来量化不确定性，无法有效识别LLM在不同领域任务中的错误，尤其是在事实性任务中表现更差。

核心思路：论文的核心思路是利用概率上下文无关文法(PCFG)来建模LLM的输出，从而更精细地捕捉LLM在生成形式化规范时的不确定性。通过分析PCFG的各种属性（如文法熵），可以获得更具区分性的不确定性信号，进而判断LLM生成结果的可靠性。这种方法考虑了形式化规范的结构信息，而不仅仅是token级别的概率。

技术框架：整体框架包含以下几个主要阶段：1) 使用LLM生成形式化规范（例如SMT公式）；2) 使用PCFG解析LLM的输出，构建语法树；3) 计算基于PCFG的各种不确定性信号（例如文法熵、规则使用频率等）；4) 使用这些不确定性信号训练分类器，判断LLM生成结果的可靠性；5) 根据分类器的结果，进行选择性验证，即只验证被认为可靠的结果。

关键创新：最重要的技术创新点在于使用PCFG来建模LLM的输出，并从中提取不确定性信号。与传统的基于token概率的方法相比，PCFG能够更好地捕捉形式化规范的结构信息，从而更准确地量化LLM的不确定性。此外，论文还提出了一个不确定性分类体系，并研究了不同任务中不确定性信号的有效性。

关键设计：PCFG的构建方式需要根据具体的形式化规范语言进行设计。论文中使用了标准的PCFG解析算法。关键参数包括PCFG的规则集、概率估计方法以及不确定性信号的计算方式。损失函数用于训练分类器，目标是区分LLM生成的正确和错误结果。选择性验证的阈值需要根据实际应用的需求进行调整，以平衡验证的准确性和效率。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，基于PCFG的不确定性量化方法能够有效识别LLM生成的错误，并在逻辑任务中AUROC>0.93。通过选择性验证，该方法能够显著减少错误（14-100%），同时保持最小的拒绝率。与直接使用LLM生成形式化规范相比，该方法能够大幅提升自动推理的可靠性。

🎯 应用场景

该研究成果可应用于各种需要自动推理的领域，例如软件验证、硬件设计、安全协议分析等。通过提高LLM生成形式化规范的可靠性，可以降低人工干预的需求，加速自动化验证流程，并最终提升系统的安全性与可靠性。未来，该方法可扩展到其他类型的形式化语言和推理任务。

📄 摘要（原文）

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic guarantees. This paper addresses this epistemological gap by comprehensively investigating failure modes and uncertainty quantification (UQ) in LLM-generated formal artifacts. Our systematic evaluation of five frontier LLMs reveals Satisfiability Modulo Theories (SMT) based autoformalization's domain-specific impact on accuracy (from +34.8% on logical tasks to -44.5% on factual ones), with known UQ techniques like the entropy of token probabilities failing to identify these errors. We introduce a probabilistic context-free grammar (PCFG) framework to model LLM outputs, yielding a refined uncertainty taxonomy. We find uncertainty signals are task-dependent (e.g., grammar entropy for logic, AUROC>0.93). Finally, a lightweight fusion of these signals enables selective verification, drastically reducing errors (14-100%) with minimal abstention, transforming LLM-driven formalization into a reliable engineering discipline.