Weave of Formal Thought

📄 arXiv: 2606.25987v1 📥 PDF

作者: Alexandre Bouayad

分类: cs.CL, cs.AI, cs.LG

发布日期: 2026-06-24

备注: Code is available at https://github.com/alexbouayad/formal

💡 一句话要点

提出WoFT以解决代码生成中的语法有效性问题

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

关键词: 大型语言模型 代码生成 语法验证 潜变量微调 结构表示 自动编程 机器学习

📋 核心要点

  1. 现有的代码生成模型在语法有效性和层次结构利用方面存在显著不足，无法保证生成代码的正确性。
  2. 本文提出了WoFT范式，通过引入形式引擎与约束解码器，结合潜变量微调方法，提升了代码生成的语法有效性。
  3. 在Python代码生成任务中，微调StarCoder2-3B模型后，模型的每个标记交叉熵相较于文本基线降低了14.3%，显示出显著的性能提升。

📝 摘要（中文）

大型语言模型（LLMs）在代码生成方面表现出色，但无法保证输出的语法有效性，也未能充分利用目标语言的层次结构。现有的约束解码框架虽然解决了语法有效性的问题，但在关键的词汇机制上存在局限，且只能近似进行词汇掩蔽，导致完整性不足。本文提出了正式思维编织（WoFT）范式，将严格的语法验证与学习的结构表示相结合。我们首先介绍了一个与Tree-sitter规范完全一致的形式引擎和约束解码器。然后，我们提出了一种潜变量微调方法，使语言模型能够在生成过程中直接交错非终结符语法符号。通过优化表面文本的加权证据下界，模型能够选择性地保留正式推导，显著提升了生成质量。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在代码生成中无法保证输出语法有效性的问题。现有方法在词汇机制和语法结构利用上存在局限，导致生成代码的质量不高。

核心思路：提出WoFT范式，通过结合严格的语法验证与学习的结构表示，提升代码生成的准确性和有效性。设计上，采用形式引擎和约束解码器来确保生成的代码符合语法规则，同时引入潜变量微调方法，使模型能够在生成过程中有效利用语法信息。

技术框架：整体架构包括形式引擎、约束解码器和潜变量微调模块。形式引擎负责语法验证，约束解码器通过增强的GLR解析与推测词法分析来生成有效的代码，而潜变量微调模块则通过优化模型的生成过程来提升结构信息的利用。

关键创新：最重要的创新在于将形式引擎与潜变量微调相结合，形成了一种新的生成机制，能够在生成过程中动态地引入语法结构信息，与传统的固定策略生成方法形成鲜明对比。

关键设计：在潜变量微调中，采用加权睡眠-觉醒（RWS）算法来优化重要性加权证据下界（IW-ELBO），使模型能够有效地选择性保留正式推导，关键参数设置和损失函数设计确保了模型的学习效率和生成质量。

🖼️ 关键图片

fig_0

📊 实验亮点

在实验中，微调后的StarCoder2-3B模型在Python代码生成任务中，相较于文本基线，模型的每个标记交叉熵降低了14.3%。这一结果表明，WoFT方法有效地恢复了传统自回归训练中丢失的关键结构信息，显著提升了生成质量。

🎯 应用场景

该研究的潜在应用领域包括自动代码生成、代码补全和智能编程助手等。通过提升代码生成的语法有效性，WoFT可以帮助开发者更高效地编写和维护代码，减少错误，提高生产力。未来，该方法可能在更广泛的编程语言和应用场景中得到推广，推动智能编程技术的发展。

📄 摘要（原文）

Large language models (LLMs) attain remarkable surface fluency on code, yet they neither formally guarantee the syntactic validity of their output nor leverage the hierarchical structure defining the target language. While existing constrained-decoding frameworks address the former, they operate under rigid assumptions that preclude critical lexical mechanisms -- including context-sensitive lexing, maximal-munch tokenization, and keyword extraction -- and only approximate vocabulary masking, sacrificing completeness. For the latter, code LLMs typically inject grammatical structure via predetermined policies rather than learning which structural information to expose. In this work, we introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations. First, we present a formal engine and constrained decoder that is sound and complete with respect to the full Tree-sitter specification. By augmenting generalized LR (GLR) parsing with a speculative-lexing construction that maintains concurrent lexer-state hypotheses synchronized with a GLR graph-structured stack, our decoder admits every subword token extending to a valid program prefix and rejects all others. Second, we present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation. Utilizing the reweighted wake-sleep (RWS) algorithm to optimize the importance-weighted evidence lower bound (IW-ELBO) of the surface text, the model learns to selectively retain formal derivations as an adaptive structural scratchpad. For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline, demonstrating that discretionary latent syntax recovers critical structural information that flat autoregressive training discards.