Grammars of Formal Uncertainty
a year ago
- #Uncertainty Quantification
- #LLMs
- #Formal Verification
- 大语言模型在自动化推理方面展现出潜力，但其概率特性与形式化验证的确定性需求存在根本矛盾。
- 本文系统研究了LLM生成形式化产物的故障模式与不确定性量化问题。
- 对五个前沿LLM的评估显示领域特性对准确率的影响显著，基于SMT的自动形式化性能波动达+34.8%至-44.5%。
- 现有不确定性量化技术（如词元概率熵）无法有效识别LLM输出错误。
- 研究提出概率上下文无关文法(PCFG)框架建模LLM输出，完善不确定性分类体系。
- 不确定性信号具有任务特异性，如在逻辑任务中文法熵的AUROC>0.93。
- 通过轻量级信号融合实现选择性验证，以最低弃用率达成错误率下降(14-100%)。
- 该方法将LLM驱动的形式化转变为可靠的工程实践。