Proposition 7：让大语言模型生成符合形式化约束的代码

Proposition 7 是一个用于大语言模型的类型感知约束生成系统，能够让 LLM 生成符合形式化语法规则的代码，支持多种编程语言范式，并提供统一的 Python API 接口。

引言：大语言模型的"幻觉"难题\n\n大语言模型（LLM）在代码生成任务中表现出色，但一个长期困扰开发者的问题是：模型生成的代码经常存在语法错误、类型不匹配或不符合特定领域约束。虽然模型可以生成"看起来正确"的代码，但在编译或运行时往往会出现问题。这种"幻觉"现象在需要严格形式化规范的场景中尤为突出。\n\nProposition 7（简称 p7）项目正是为了解决这一问题而生。它是一个系统无关的形式化约束生成框架，能够让大语言模型在生成代码时严格遵守预定义的语法规则和类型系统。\n\n## 项目概述\n\nProposition 7 由 Unsuspicious Industries 开发，是一个面向大语言模型的类型感知约束生成系统。其核心目标是让 LLM 生成的输出不仅语法正确，而且符合特定的形式化规范。\n\n与传统的代码生成工具不同，p7 不是在生成后进行验证和修正，而是在生成过程中就施加约束，确保每一个 token 的选择都符合语法规则。这种方法从根本上避免了无效代码的产生。\n\n## 核心技术原理\n\n### 约束解码机制\n\np7 的核心技术是"约束解码"（Constrained Decoding）。在传统的 LLM 生成过程中，模型在每个步骤都会选择概率最高的下一个 token。而在 p7 中，系统会首先检查哪些 token 是语法允许的，然后只从这些合法选项中进行选择。\n\n具体来说，p7 使用了一种称为"语法引导生成"的技术。它维护一个当前语法状态，并根据已生成的内容动态更新允许的 token 集合。这类似于编译器在解析代码时的状态机，但反向运行——不是解析已有代码，而是指导代码的生成。\n\n### 内置语法支持\n\np7 预置了多种形式化语法的支持，包括：\n\n- stlc（Simply Typed Lambda Calculus）：简单类型 lambda 演算，函数式编程的理论基础\n- fun（ML-style functional expressions）：ML 风格的函数式表达式，适用于 Haskell、OCaml 等语言的子集\n- imp（Typed imperative programs）：类型化的命令式程序，支持类 C 语言的子集\n- toy（Small typed toy grammar）：小型教学用类型语法，适合入门学习\n\n这些语法规范使用 .auf 格式定义，用户也可以自定义新的语法规则。\n\n## 使用方法与 API 设计\n\n### 高层便捷接口\n\n对于快速原型开发，p7 提供了简单的高层 API：\n\npython\nimport proposition7\n\nresult = proposition7.generate(\n \"identity function\",\n model=\"gpt2\",\n grammar=\"stlc\",\n initial=\"λx:Int.\",\n max_tokens=20,\n)\n\n\n这段代码会让模型生成一个恒等函数，且保证输出符合简单类型 lambda 演算的语法规则。\n\n### 本地模型封装\n\n对于需要更多控制的场景，p7 提供了 ConstrainedModel 类：\n\npython\nimport proposition7\n\nmodel = proposition7.ConstrainedModel.from_pretrained(\n \"gpt2\",\n grammar=proposition7.get_grammar(\"fun\"),\n device=\"cpu\",\n)\n\nresult = model.generate_constrained(\n prompt=\"Define inc:Int->Int and call it on 1. Output only program text.\",\n initial=\"let inc: Int -> Int = (n: Int) =>\",\n max_tokens=64,\n)\n\n\n同一个模型实例也支持无约束生成，方便对比实验：\n\npython\nresult = model.generate_unconstrained(\n prompt=\"Write a short typed function example.\",\n max_tokens=64,\n top_k=50,\n temperature=0.8,\n)\n\n\n## 项目架构与代码组织\n\np7 的代码库结构清晰，主要分为以下几个部分：\n\n- src/proposition7/：核心 Python 包\n - api.py：高层 API 和会话管理\n - llm.py：约束模型封装\n - inference.py：底层约束生成循环\n - environment.py：可选推理环境\n - grammars/：内置语法规范\n - models/：模型适配器\n\n- benchmarks/：基准测试框架\n - run.py：TOML 驱动的测试运行器\n - configs/：测试配置\n - agg.py：结果聚合分析\n\n- tests/：pytest 测试套件\n\n## 应用场景与价值\n\n### 教育领域\n\n在编程教育中，p7 可以帮助学生生成符合特定语言规范的代码示例，避免因语法错误而分散注意力。教师可以定义特定的语法子集，让学生在这个安全的环境中练习。\n\n### 形式化验证\n\n对于需要形式化验证的系统，p7 可以确保生成的代码从一开始就符合规范，减少后续验证的工作量。这在安全关键系统开发中尤为重要。\n\n### 领域特定语言（DSL）\n\np7 的语法系统可以轻松扩展以支持自定义的领域特定语言。企业可以定义自己的 DSL 语法，然后使用 p7 让 LLM 生成符合该语法的代码。\n\n### 代码补全与重构\n\n在 IDE 插件中集成 p7，可以实现智能的、语法感知的代码补全。当用户开始输入时，系统可以预测并建议符合语法的后续代码。\n\n## 技术亮点与创新\n\n### 系统无关性\n\np7 被设计为"系统无关"的框架，意味着它不依赖于特定的 LLM 提供商或部署方式。目前支持 Hugging Face Transformers 本地模型，未来可以扩展到其他后端。\n\n### 形式化基础\n\n与许多基于启发式的代码生成工具不同，p7 建立在坚实的形式化理论基础之上。它使用类型系统和语法规则来指导生成，而不是简单的模式匹配或后处理过滤。\n\n### 灵活的部署方式\n\n项目提供了多种使用方式：可以直接安装 Python 包使用，也可以通过 Docker 镜像部署，还支持 Nix 开发环境。这种灵活性使得 p7 可以适应不同的工作流程和基础设施。\n\n## 未来展望\n\n随着大语言模型在软件开发中的应用越来越广泛，对生成内容的质量控制需求也日益增长。Proposition 7 展示了一种有前景的技术方向：将形式化方法与现代 AI 相结合，在保证生成灵活性的同时确保输出的正确性。\n\n未来，我们可以期待看到更多类似的约束生成技术出现，不仅应用于代码生成，还可能扩展到自然语言处理的其他领域，如结构化数据生成、配置文件编写等。\n\n## 结语\n\nProposition 7 为大语言模型的应用提供了一个重要的安全网。通过形式化约束，它让 LLM 从"可能正确"走向"一定符合规范"。对于需要高可靠性的应用场景，这种技术无疑具有重要的实用价值。\n\n项目代码已在 GitHub 开源，感兴趣的开发者可以尝试集成到自己的工具链中，体验约束生成带来的代码质量提升。

引言：大语言模型的"幻觉"难题\n\n大语言模型（LLM）在代码生成任务中表现出色，但一个长期困扰开发者的问题是：模型生成的代码经常存在语法错误、类型不匹配或不符合特定领域约束。虽然模型可以生成"看起来正确"的代码，但在编译或运行时往往会出现问题。这种"幻觉"现象在需要严格形式化规范的场景中尤为突出。\n\nProposition 7（简称 p7）项目正是为了解决这一问题而生。它是一个系统无关的形式化约束生成框架，能够让大语言模型在生成代码时严格遵守预定义的语法规则和类型系统。\n\n项目概述\n\nProposition 7 由 Unsuspicious Industries 开发，是一个面向大语言模型的类型感知约束生成系统。其核心目标是让 LLM 生成的输出不仅语法正确，而且符合特定的形式化规范。\n\n与传统的代码生成工具不同，p7 不是在生成后进行验证和修正，而是在生成过程中就施加约束，确保每一个 token 的选择都符合语法规则。这种方法从根本上避免了无效代码的产生。\n\n核心技术原理\n\n约束解码机制\n\np7 的核心技术是"约束解码"（Constrained Decoding）。在传统的 LLM 生成过程中，模型在每个步骤都会选择概率最高的下一个 token。而在 p7 中，系统会首先检查哪些 token 是语法允许的，然后只从这些合法选项中进行选择。\n\n具体来说，p7 使用了一种称为"语法引导生成"的技术。它维护一个当前语法状态，并根据已生成的内容动态更新允许的 token 集合。这类似于编译器在解析代码时的状态机，但反向运行——不是解析已有代码，而是指导代码的生成。\n\n内置语法支持\n\np7 预置了多种形式化语法的支持，包括：\n\n- stlc（Simply Typed Lambda Calculus）：简单类型 lambda 演算，函数式编程的理论基础\n- fun（ML-style functional expressions）：ML 风格的函数式表达式，适用于 Haskell、OCaml 等语言的子集\n- imp（Typed imperative programs）：类型化的命令式程序，支持类 C 语言的子集\n- toy（Small typed toy grammar）：小型教学用类型语法，适合入门学习\n\n这些语法规范使用 .auf 格式定义，用户也可以自定义新的语法规则。\n\n使用方法与 API 设计\n\n高层便捷接口\n\n对于快速原型开发，p7 提供了简单的高层 API：\n\npython\nimport proposition7\n\nresult = proposition7.generate(\n \"identity function\",\n model=\"gpt2\",\n grammar=\"stlc\",\n initial=\"λx:Int.\",\n max_tokens=20,\n)\n\n\n这段代码会让模型生成一个恒等函数，且保证输出符合简单类型 lambda 演算的语法规则。\n\n本地模型封装\n\n对于需要更多控制的场景，p7 提供了 ConstrainedModel 类：\n\npython\nimport proposition7\n\nmodel = proposition7.ConstrainedModel.from_pretrained(\n \"gpt2\",\n grammar=proposition7.get_grammar(\"fun\"),\n device=\"cpu\",\n)\n\nresult = model.generate_constrained(\n prompt=\"Define inc:Int->Int and call it on 1. Output only program text.\",\n initial=\"let inc: Int -> Int = (n: Int) =>\",\n max_tokens=64,\n)\n\n\n同一个模型实例也支持无约束生成，方便对比实验：\n\npython\nresult = model.generate_unconstrained(\n prompt=\"Write a short typed function example.\",\n max_tokens=64,\n top_k=50,\n temperature=0.8,\n)\n\n\n项目架构与代码组织\n\np7 的代码库结构清晰，主要分为以下几个部分：\n\n- src/proposition7/：核心 Python 包\n - api.py：高层 API 和会话管理\n - llm.py：约束模型封装\n - inference.py：底层约束生成循环\n - environment.py：可选推理环境\n - grammars/：内置语法规范\n - models/：模型适配器\n\n- benchmarks/：基准测试框架\n - run.py：TOML 驱动的测试运行器\n - configs/：测试配置\n - agg.py：结果聚合分析\n\n- tests/：pytest 测试套件\n\n应用场景与价值\n\n教育领域\n\n在编程教育中，p7 可以帮助学生生成符合特定语言规范的代码示例，避免因语法错误而分散注意力。教师可以定义特定的语法子集，让学生在这个安全的环境中练习。\n\n形式化验证\n\n对于需要形式化验证的系统，p7 可以确保生成的代码从一开始就符合规范，减少后续验证的工作量。这在安全关键系统开发中尤为重要。\n\n领域特定语言（DSL）\n\np7 的语法系统可以轻松扩展以支持自定义的领域特定语言。企业可以定义自己的 DSL 语法，然后使用 p7 让 LLM 生成符合该语法的代码。\n\n代码补全与重构\n\n在 IDE 插件中集成 p7，可以实现智能的、语法感知的代码补全。当用户开始输入时，系统可以预测并建议符合语法的后续代码。\n\n技术亮点与创新\n\n系统无关性\n\np7 被设计为"系统无关"的框架，意味着它不依赖于特定的 LLM 提供商或部署方式。目前支持 Hugging Face Transformers 本地模型，未来可以扩展到其他后端。\n\n形式化基础\n\n与许多基于启发式的代码生成工具不同，p7 建立在坚实的形式化理论基础之上。它使用类型系统和语法规则来指导生成，而不是简单的模式匹配或后处理过滤。\n\n灵活的部署方式\n\n项目提供了多种使用方式：可以直接安装 Python 包使用，也可以通过 Docker 镜像部署，还支持 Nix 开发环境。这种灵活性使得 p7 可以适应不同的工作流程和基础设施。\n\n未来展望\n\n随着大语言模型在软件开发中的应用越来越广泛，对生成内容的质量控制需求也日益增长。Proposition 7 展示了一种有前景的技术方向：将形式化方法与现代 AI 相结合，在保证生成灵活性的同时确保输出的正确性。\n\n未来，我们可以期待看到更多类似的约束生成技术出现，不仅应用于代码生成，还可能扩展到自然语言处理的其他领域，如结构化数据生成、配置文件编写等。\n\n结语\n\nProposition 7 为大语言模型的应用提供了一个重要的安全网。通过形式化约束，它让 LLM 从"可能正确"走向"一定符合规范"。对于需要高可靠性的应用场景，这种技术无疑具有重要的实用价值。\n\n项目代码已在 GitHub 开源，感兴趣的开发者可以尝试集成到自己的工具链中，体验约束生成带来的代码质量提升。