标题： 形式不确定性语法：何时信任大型语言模型在自动化推理任务中的应用 显示英文标题

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

摘要： 大型语言模型（LLMs）在通过生成正式规范来实现自动化推理的普及方面展现出非凡的潜力。然而，存在一个根本性的矛盾：LLMs 是概率性的，而形式验证需要确定性保证。本文通过全面研究 LLM 生成的形式化工件中的失效模式和不确定性量化（UQ），解决了这一认识论差距。我们对五种前沿 LLM 的系统评估揭示了基于可满足模理论（SMT）的自动形式化在准确性方面的领域特定影响（从逻辑任务上的 +34.8% 到事实任务上的 -44.5%），并且已知的 UQ 技术如标记概率的熵未能识别这些错误。我们引入了一种概率上下文无关语法（PCFG）框架来建模 LLM 输出，从而产生了一个细化的不确定性分类。我们发现不确定性信号是任务依赖的（例如，逻辑中的语法熵，AUROC > 0.93）。最后，这些信号的轻量级融合实现了选择性验证，大幅减少了错误（14%-100%），且弃权率极低，将 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.