FASTRIC: Prompt Specification Language for Verifiable LLM Interactions

📄 arXiv: 2512.18940v1 📥 PDF

作者: Wen-Long Jin

分类: cs.CL, cs.SE

发布日期: 2025-12-22

备注: 13 pages, 3 figures. Supplementary materials at https://doi.org/10.17605/OSF.IO/PV6R3

💡 一句话要点

FASTRIC：一种用于可验证LLM交互的提示规范语言

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

关键词: 大型语言模型 多轮交互 形式化规范 提示工程 有限状态机

📋 核心要点

  1. 现有LLM多轮交互缺乏形式化规范，难以验证其执行是否符合设计意图，存在不可控风险。
  2. FASTRIC通过提示规范语言显式表达有限状态机，使LLM作为智能代理执行指定行为，实现可验证的交互。
  3. 实验表明，最佳规范形式化程度与模型容量相关，存在模型特定的“金发姑娘区”，可实现最佳一致性。

📝 摘要（中文）

大型语言模型(LLMs)执行复杂的多轮交互协议，但缺乏正式规范来验证执行是否符合设计者的意图。我们引入FASTRIC，一种提示规范语言，它在自然语言提示中显式地表达了隐式的有限状态机(FSMs)，从而可以通过执行轨迹分析进行一致性验证。LLM充当智能执行代理：解释设计者编码的FSMs以执行指定的行为角色。与需要解析器和编译器的符号规范语言不同，FASTRIC利用LLMs作为统一的基础设施——同时充当解析器、解释器、运行时环境和开发助手。FASTRIC指导设计者阐明七个FSM元素（最终状态、代理、状态、触发器、角色、初始状态、约束），从而构建多轮交互。规范的形式化程度——从前沿模型推断的隐式描述到为较弱模型提供的逐步指令——可以作为一个设计参数。我们引入程序一致性作为验证指标，衡量执行对FSM规范的遵守程度。在一个包含四个形式化级别和三个模型规模（14.7B、685B、1T+参数）的3状态幼儿园辅导FSM测试中，结果表明最佳规范形式化程度是模型容量的函数。DeepSeek-V3.2 (685B)在L2-L4级别上实现了完美的一致性(1.00)；ChatGPT-5 (~1T)在L3级别达到峰值(0.90)，然后在L4级别崩溃(0.39)；Phi4 (14.7B)没有显示出稳定的最优值，具有较高的方差(SD=0.16-0.36)。这些发现揭示了模型特定的形式化范围——“金发姑娘区”——其中规范提供了足够的结构而没有过度约束，从而建立了提示规范工程，用于创建可验证的交互协议，将多轮交互设计从启发式艺术转变为具有可衡量的程序保证的系统工程。

🔬 方法详解

问题定义：论文旨在解决大型语言模型在多轮交互中缺乏形式化规范的问题。现有方法依赖于隐式的、非结构化的提示，导致LLM的行为难以预测和验证，无法保证其执行符合设计者的意图。这使得多轮交互设计成为一种启发式艺术，缺乏可衡量的程序保证。

核心思路：论文的核心思路是引入一种提示规范语言FASTRIC，将隐式的有限状态机（FSM）显式地表达在自然语言提示中。通过这种方式，LLM可以被视为一个智能执行代理，它解释设计者编码的FSM，并按照规范执行指定的行为角色。这种方法将多轮交互设计从一种启发式艺术转变为一种具有可衡量的程序保证的系统工程。

技术框架：FASTRIC的技术框架包括以下几个主要组成部分：1) 提示规范语言：用于描述FSM的七个关键元素，包括最终状态、代理、状态、触发器、角色、初始状态和约束。2) LLM作为统一基础设施：利用LLM同时充当解析器、解释器、运行时环境和开发助手。3) 程序一致性验证：通过执行轨迹分析，衡量LLM的执行是否符合FSM规范。4) 形式化程度设计参数：允许设计者根据模型容量调整规范的形式化程度，从隐式描述到显式指令。

关键创新：FASTRIC的关键创新在于它将形式化规范引入到LLM的提示工程中，从而实现了可验证的多轮交互。与传统的符号规范语言不同，FASTRIC利用LLM自身的能力来解析和执行规范，无需额外的解析器和编译器。此外，FASTRIC还提出了程序一致性作为一种新的验证指标，用于衡量LLM的执行是否符合FSM规范。

关键设计：FASTRIC的关键设计包括：1) FSM元素的显式表达：通过提示规范语言，清晰地定义FSM的七个关键元素。2) 形式化程度的灵活调整：允许设计者根据模型容量调整规范的形式化程度，以达到最佳的性能。3) 程序一致性的量化评估：通过执行轨迹分析，量化评估LLM的执行是否符合FSM规范。4) 模型容量与形式化程度的关联：实验结果表明，最佳规范形式化程度是模型容量的函数，存在模型特定的“金发姑娘区”。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，最佳规范形式化程度与模型容量相关。DeepSeek-V3.2 (685B)在L2-L4级别上实现了完美的一致性(1.00)；ChatGPT-5 (~1T)在L3级别达到峰值(0.90)，然后在L4级别崩溃(0.39)；Phi4 (14.7B)没有显示出稳定的最优值，具有较高的方差(SD=0.16-0.36)。这些结果揭示了模型特定的形式化范围，即“金发姑娘区”。

🎯 应用场景

FASTRIC可应用于各种需要可验证多轮交互的场景，如智能客服、教育辅导、任务自动化等。它能够提高LLM应用的可靠性和安全性，降低风险，并为多轮交互设计提供系统化的工程方法。未来，FASTRIC有望推动LLM在安全敏感领域的应用，例如医疗诊断、金融风控等。

📄 摘要（原文）

Large Language Models (LLMs) execute complex multi-turn interaction protocols but lack formal specifications to verify execution against designer intent. We introduce FASTRIC, a Prompt Specification Language that makes implicit Finite State Machines (FSMs) explicit in natural language prompts, enabling conformance verification through execution trace analysis. The LLM serves as intelligent execution agent: interpreting designer-encoded FSMs to execute specified behavioral roles. Unlike symbolic specification languages requiring parsers and compilers, FASTRIC leverages LLMs as unified infrastructure-simultaneously parser, interpreter, runtime environment, and development assistant. FASTRIC guides designers to articulate seven FSM elements (Final States, Agents, States, Triggers, Roles, Initial State, Constraints) structuring multi-turn interactions. Specification formality-ranging from implicit descriptions that frontier models infer to explicit step-by-step instructions for weaker models-serves as a design parameter. We introduce procedural conformance as verification metric measuring execution adherence to FSM specifications. Testing a 3-state kindergarten tutoring FSM across four formality levels and three model scales (14.7B, 685B, 1T+ parameters) reveals optimal specification formality is a function of model capacity. DeepSeek-V3.2 (685B) achieves perfect conformance (1.00) at L2-L4; ChatGPT-5 (~1T) peaks at L3 (0.90) before collapsing at L4 (0.39); Phi4 (14.7B) shows no stable optimum with high variance (SD=0.16-0.36). These findings reveal model-specific formality ranges-"Goldilocks zones"-where specifications provide sufficient structure without over-constraint, establishing Prompt Specification Engineering for creating verifiable interaction protocols, transforming multi-turn interaction design from heuristic art to systematic engineering with measurable procedural guarantees.