让大模型生成的逻辑代码更可信：提出新方法量化不确定性
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
- 用概率上下文无关语法建模大模型输出，识别不同任务下的错误模式
- 在逻辑任务上提升准确率34.8%，在事实类任务上降低44.5%但可检测
- 融合多信号实现选择性验证，误判减少14%-100%，适合高可靠性场景
大语言模型在自动化推理中生成形式化规范展现出巨大潜力，但其概率本质与形式验证所需的确定性之间存在根本矛盾。本文系统研究了大模型生成形式化产物中的失败模式与不确定性量化（UQ）问题。对五种前沿大模型的评估显示，基于SMT的自动形式化在逻辑任务上准确率提升34.8%，而在事实类任务上下降44.5%；现有不确定性量化方法（如词元概率熵）无法有效识别这些错误。为此，我们提出一种概率上下文无关语法（PCFG）框架，构建更精细的不确定性分类体系。发现不确定性信号具有任务依赖性（如逻辑任务用语法熵，AUROC > 0.93）。最终，通过轻量级信号融合实现选择性验证，在仅少量拒绝的情况下，将错误率降低14%-100%，使大模型驱动的形式化迈向可靠工程实践。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。