TerraFormer: Automated Infrastructure-as-Code with LLMs Fine-Tuned via Policy-Guided Verifier Feedback

📄 arXiv: 2601.08734v1 📥 PDF

作者: Prithwish Jana, Sam Davidson, Bhavana Bhasker, Andrey Kan, Anoop Deoras, Laurent Callot

分类: cs.SE, cs.AI

发布日期: 2026-01-13

备注: The paper has been published at the 2026 IEEE/ACM 48th International Conference on Software Engineering (ICSE 2026), Rio de Janeiro, Brazil, April 12-18, 2026

DOI: 10.1145/3786583.3786898

💡 一句话要点

TerraFormer：利用策略引导的验证器反馈微调LLM，实现基础设施即代码的自动化生成。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 基础设施即代码 大型语言模型 神经符号方法 形式验证 强化学习 自动化 云基础设施 DevOps

📋 核心要点

  1. 现有方法难以从自然语言生成正确的IaC配置，大型语言模型（LLM）容易产生错误配置。
  2. TerraFormer采用神经符号框架，结合监督微调和验证器引导的强化学习，利用形式验证工具提供反馈。
  3. 实验结果表明，TerraFormer显著提高了IaC生成的正确率，并在多个数据集上优于更大的LLM模型。

📝 摘要（中文）

本文提出TerraFormer，一个用于IaC生成和修改的神经符号框架，它结合了监督微调和验证器引导的强化学习，使用形式验证工具来提供关于语法、可部署性和策略合规性的反馈。作者通过多阶段验证和迭代LLM自校正，构建了两个大型高质量的NL-to-IaC数据集，TF-Gen（152k个实例）和TF-Mutn（52k个实例）。针对17个最先进的LLM（包括~50倍更大的模型，如Sonnet 3.7、DeepSeek-R1和GPT-4.1）的评估表明，TerraFormer相对于其基础LLM，在IaC-Eval上提高了15.94%的正确率，在TF-Gen (Test)上提高了11.65%，在TF-Mutn (Test)上提高了19.60%。它在TF-Gen (Test)和TF-Mutn (Test)上优于更大的模型，在IaC-Eval上排名第三，并实现了最高的最佳实践和安全合规性。

🔬 方法详解

问题定义：论文旨在解决从自然语言描述自动生成正确且符合规范的Infrastructure-as-Code (IaC)配置的问题。现有方法，特别是直接使用大型语言模型（LLM），容易产生语法错误、部署失败或违反安全策略的IaC代码，导致自动化程度低且风险高。

核心思路：TerraFormer的核心思路是结合LLM的生成能力和形式验证工具的精确验证能力，通过神经符号方法实现IaC的自动生成和优化。具体来说，利用验证器对LLM生成的代码进行多方面的检查，并将验证结果作为反馈信号，指导LLM进行迭代改进。

技术框架：TerraFormer框架包含以下几个主要模块：1) LLM生成器：使用微调后的LLM从自然语言描述生成初始的IaC代码。2) 验证器：使用形式验证工具对生成的IaC代码进行语法、可部署性和策略合规性检查。3) 奖励函数：根据验证器的反馈结果，设计奖励函数，用于强化学习过程。4) 强化学习模块：使用强化学习算法，根据奖励函数优化LLM的生成策略，使其生成更符合规范的IaC代码。

关键创新：TerraFormer的关键创新在于将形式验证工具集成到LLM的训练循环中，通过验证器提供的反馈信号，指导LLM进行迭代改进。这种神经符号方法有效地结合了LLM的生成能力和形式验证的精确性，显著提高了IaC生成的正确性和可靠性。

关键设计：论文设计了多阶段验证流程，包括语法检查、部署检查和策略合规性检查。奖励函数的设计考虑了多个因素，包括代码的正确性、可部署性和安全性。此外，论文还构建了两个大型高质量的NL-to-IaC数据集，用于LLM的微调和评估。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

TerraFormer在IaC-Eval、TF-Gen (Test)和TF-Mutn (Test)数据集上分别比其基础LLM提高了15.94%、11.65%和19.60%的正确率。在TF-Gen (Test)和TF-Mutn (Test)上，TerraFormer优于更大的模型（如Sonnet 3.7、DeepSeek-R1和GPT-4.1），并在IaC-Eval上排名第三，同时实现了最高的最佳实践和安全合规性。

🎯 应用场景

TerraFormer可应用于云基础设施自动化管理、DevOps流程优化、安全合规性自动检查等领域。通过自动生成和验证IaC代码，可以显著提高云资源配置的效率和安全性，降低运维成本，并加速软件交付流程。该研究对推动基础设施即代码的自动化和智能化具有重要意义。

📄 摘要（原文）

Automating Infrastructure-as-Code (IaC) is challenging, and large language models (LLMs) often produce incorrect configurations from natural language (NL). We present TerraFormer, a neuro-symbolic framework for IaC generation and mutation that combines supervised fine-tuning with verifier-guided reinforcement learning, using formal verification tools to provide feedback on syntax, deployability, and policy compliance. We curate two large, high-quality NL-to-IaC datasets, TF-Gen (152k instances) and TF-Mutn (52k instances), via multi-stage verification and iterative LLM self-correction. Evaluations against 17 state-of-the-art LLMs, including ~50x larger models like Sonnet 3.7, DeepSeek-R1, and GPT-4.1, show that TerraFormer improves correctness over its base LLM by 15.94% on IaC-Eval, 11.65% on TF-Gen (Test), and 19.60% on TF-Mutn (Test). It outperforms larger models on both TF-Gen (Test) and TF-Mutn (Test), ranks third on IaC-Eval, and achieves top best-practices and security compliance.