TOGGLE: Temporal Logic-Guided Large Language Model Compression for Edge

📄 arXiv: 2512.16855v1 📥 PDF

作者: Khurram Khalil, Khaza Anuarul Hoque

分类: cs.AI, cs.LO

发布日期: 2025-12-18

备注: Published in the IEEE ICCAD 2025 conference

DOI: 10.1109/ICCAD66269.2025.11240962

💡 一句话要点

提出TOGGLE，通过时序逻辑引导LLM压缩，实现边缘设备高效部署。

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

关键词: 大语言模型压缩 边缘计算 形式化方法 信号时序逻辑 贝叶斯优化

📋 核心要点

  1. 现有LLM压缩方法在降低计算成本的同时，往往会损害模型的关键语言属性，且缺乏形式化保证。
  2. TOGGLE利用信号时序逻辑(STL)来形式化地指定和强制执行压缩过程中的语言属性，保证压缩后的模型满足特定约束。
  3. 实验表明，TOGGLE在降低计算成本和模型大小的同时，能够保持LLM的语言属性，并在边缘设备上实现高效部署。

📝 摘要（中文）

大型语言模型(LLM)在自然语言任务中表现出色，但需要大量的计算资源，限制了其在资源受限的边缘设备上的部署。现有的压缩技术，如量化和剪枝，通常会降低关键的语言属性，并且缺乏对模型行为保持的正式保证。我们提出了时间逻辑引导的大型语言模型压缩(TOGGLE)，这是一个新颖的框架，它利用信号时序逻辑(STL)来正式地指定和强制执行压缩过程中的语言属性。TOGGLE采用STL鲁棒性引导的贝叶斯优化，系统地探索逐层量化和剪枝配置，生成压缩模型，在不进行重新训练或微调的情况下，正式地满足指定的语言约束。在四个LLM架构(GPT-2, DeepSeek-V2 7B, LLaMA 3 8B, 和 Mistral 7B)上评估TOGGLE，我们实现了高达3.3倍的计算成本(FLOPs)降低和高达68.8%的模型大小降低，同时满足所有语言属性。TOGGLE代表了形式化方法首次集成到LLM压缩中，从而能够在边缘硬件上高效、可验证地部署LLM。

🔬 方法详解

问题定义：论文旨在解决大型语言模型（LLM）在资源受限的边缘设备上部署的问题。现有压缩方法，如量化和剪枝，虽然能降低计算成本，但往往会损害LLM的关键语言属性，并且缺乏对模型行为保持的正式保证。这些方法无法确保压缩后的模型仍然满足特定的语言约束，例如语法正确性或语义一致性。

核心思路：TOGGLE的核心思路是利用信号时序逻辑（STL）来形式化地指定和强制执行压缩过程中的语言属性。通过将语言属性编码为STL公式，TOGGLE可以在压缩过程中评估模型的行为是否满足这些属性。这种方法允许在不进行重新训练或微调的情况下，生成满足特定语言约束的压缩模型。

技术框架：TOGGLE框架主要包含以下几个阶段：1) STL属性定义：根据具体的语言任务，定义需要保持的语言属性，并将其形式化为STL公式。2) 鲁棒性评估：使用STL鲁棒性度量来评估模型满足STL公式的程度。鲁棒性越高，表示模型越能可靠地满足相应的语言属性。3) 贝叶斯优化：利用贝叶斯优化算法，系统地探索逐层量化和剪枝配置。优化目标是最小化计算成本（FLOPs）和模型大小，同时最大化STL鲁棒性。4) 模型压缩：根据贝叶斯优化得到的最佳配置，对LLM进行量化和剪枝，生成压缩后的模型。

关键创新：TOGGLE的关键创新在于将形式化方法（STL）引入到LLM压缩中。与传统的压缩方法不同，TOGGLE能够提供对模型行为的正式保证，确保压缩后的模型仍然满足特定的语言约束。这是首次将形式化验证技术应用于LLM压缩领域。

关键设计：TOGGLE的关键设计包括：1) STL公式的选择：选择合适的STL公式来准确地描述需要保持的语言属性。2) 鲁棒性度量的定义：定义合适的鲁棒性度量来评估模型满足STL公式的程度。3) 贝叶斯优化算法的选择：选择合适的贝叶斯优化算法来高效地探索压缩配置空间。4) 量化和剪枝策略：选择合适的量化和剪枝策略来平衡计算成本和模型性能。

📊 实验亮点

TOGGLE在GPT-2、DeepSeek-V2 7B、LLaMA 3 8B和Mistral 7B等LLM架构上进行了评估，实现了高达3.3倍的计算成本(FLOPs)降低和高达68.8%的模型大小降低，同时满足所有指定的语言属性。这些结果表明，TOGGLE能够在显著降低计算资源需求的同时，保持LLM的语言能力。

🎯 应用场景

TOGGLE可应用于各种边缘计算场景，例如智能手机、物联网设备和自动驾驶汽车。通过在边缘设备上部署压缩后的LLM，可以实现本地化的自然语言处理，提高响应速度和隐私保护。该研究成果对于推动LLM在资源受限环境下的广泛应用具有重要意义，并有望促进边缘智能的发展。

📄 摘要（原文）

Large Language Models (LLMs) deliver exceptional performance across natural language tasks but demand substantial computational resources, limiting their deployment on resource-constrained edge devices. Existing compression techniques, such as quantization and pruning, often degrade critical linguistic properties and lack formal guarantees for preserving model behavior. We propose Temporal Logic-Guided Large Language Model Compression (TOGGLE), a novel framework that leverages Signal Temporal Logic (STL) to formally specify and enforce linguistic properties during compression. TOGGLE employs an STL robustness-guided Bayesian optimization to systematically explore layer-wise quantization and pruning configurations, generating compressed models that formally satisfy specified linguistic constraints without retraining or fine-tuning. Evaluating TOGGLE on four LLM architectures (GPT-2, DeepSeek-V2 7B, LLaMA 3 8B, and Mistral 7B), we achieve up to 3.3x reduction in computational costs (FLOPs) and up to a 68.8% reduction in model size while satisfying all linguistic properties. TOGGLE represents the first integration of formal methods into LLM compression, enabling efficient, verifiable deployment of LLMs on edge hardware.