Learn2Zinc：针对MiniZinc中文本到模型翻译的小语言模型微调

# Learn2Zinc：面向MiniZinc文本到模型翻译的小语言模型微调

来源：https://arxiv.org/html/2607.20456

Serdar Kadıoğlu¹,² 和 Karthik Uppuluri¹

¹AI卓越中心，富达投资  
²计算机科学系，布朗大学  
[email protected]

###### 摘要

大型语言模型在主流编程语言的代码生成方面表现出色，但在处理罕见、领域特定的语言（如用于组合问题的约束建模语言MiniZinc）时则力不从心。我们研究目标微调是否能够教会小语言模型（参数规模0.6B至20B）从自然语言问题描述生成语法正确且语义有效的MiniZinc模型。我们的关键发现是：在使用这种领域特定语言时，语法错误主导了失败——Qwen3、LLaMa、Gemma和GPT-OSS等小语言模型的开箱执行准确率几乎为零。我们提出了一种跨模型错误引导方法，收集多次LLM运行中的语法错误，并利用这些错误构建一个纠错训练数据集。该数据集允许我们微调小语言模型，在直接代码生成和思维链方法上均持续改进所有模型规模的表现。结合自我反思和集成方法，我们的方法实现了高达98%的执行准确率。同时，解准确率仍保持在35%，表明语法是可学的，但约束推理仍然是一个挑战。我们将微调流程、数据集和模型开源，以促进文本到模型翻译的进一步研究。

## 1 引言

优化技术取得了显著进展，从求解器效率的大幅提升到高级建模语言的发展以增强可用性。然而，基本的决策框架几十年来保持不变，遵循着事实上的“建模并运行”策略。在这种现状下，用户需要手动将问题描述转化为优化模型，然后由求解器处理以获得解。多年来，高级建模语言如MiniZinc（Nethercote等人，2007）、CPMpy（Guns，2019）和GAMS（Bussieck and Meeraus，2004）通过提供求解器无关的方法部分解决了可访问性挑战，这些方法强大且灵活。这些建模框架使从业者能够专注于描述问题，而无需担心具体的求解方法，尤其适用于需求经常变化的实际应用。然而，将问题描述转化为形式化约束模型的认知障碍依然存在。这种障碍尤其严重，因为深入理解问题领域的领域专家往往缺乏形式化建模所需的专业知识。由此产生的对建模专家的依赖造成了操作瓶颈，并可能导致翻译过程中对领域特定需求的误解。

与此同时，大型语言模型（LLMs）已成为与机器通信的媒介（OpenAI等人，2024；Team等人，2025；DeepSeek-AI等人，2025）。虽然语言模型在自然文本交互方面能力强大，但在形式化、声明式方法所需的一致性和精确性方面却存在困难，从基本的类型声明到复杂的约束关系。它们在处理文本到模型翻译所需的数学和逻辑推理时面临重大挑战（Simchi-Levi等人，2025；Wasserkrug等人，2025；Kadıoğlu等人，2024）¹¹¹https://skadio.github.io/text2model。目前理解文本描述并将其转化为问题表述之间的差距表明，建模助手方面还需要更多工作。

激励本工作的一个关键观察是，MiniZinc作为一种领域特定语言，在典型的LLM预训练语料库中的代表性远低于Python、C++或Java等成熟语言。从视角来看，GitHub上MiniZinc的主题页面列出的仓库数量约为数百个，而Python或JavaScript则有数百万个。这种有限的存在意味着LLM在预训练期间对MiniZinc语法的接触极少。支持这一观察的是，我们测试的五个模型中有四个（Qwen3、LLaMa和Gemini）在MiniZinc生成上的执行准确率为0.0%，而最大的模型（GPT-OSS-20B）也仅达到6.0%。这证实了MiniZinc明显超出了当前最佳小语言模型的分布范围。这提出了一个基本的研究问题：有针对性的微调能否教会小语言模型一种领域特定的编程语言，如MiniZinc？这正是我们在本文中研究的内容。

### 1.1 我们的贡献

我们的贡献如下：

1. 我们首次系统研究了从0.6B到20B参数规模的小语言模型微调用于MiniZinc代码生成。
2. 为了使微调成为可能，我们引入了一种跨模型错误引导方法，收集多次LLM运行中的语法错误，并利用这些错误创建一个真实的纠错训练数据集。
3. 我们提出了三种复杂度递增的微调策略，并表明使用纠错示例增强训练数据在所有模型规模上均持续优于直接代码生成和思维链方法。
4. 使用我们微调模型的集成，我们实现了98%的执行准确率，从0.0%-6.0%的开箱准确率提升，有效解决了MiniZinc语法问题。同时，我们将约束推理识别为剩余瓶颈，解准确率仅为35%，并对错误模式进行了详细分析。
5. 我们将微调流程、数据集和模型开源，以促进文本到模型翻译的进一步研究。

## 2 背景

让我们简要回顾本研究中使用的约束建模语言MiniZinc、用于基准测试的数据集Text2Zinc，以及我们的LLM副驾驶方法Text2Model。

### 2.1 MiniZinc

MiniZinc（Nethercote等人，2007）是一种高级约束建模语言，支持离散和连续优化及满足问题。其求解器无关的设计允许与各种求解器后端通信，包括约束编程（CP）、（混合）整数规划（MIP）和布尔可满足性/延迟子句生成（SAT）。这种灵活性通过编译到FlatZinc（一种与不同求解器接口的中间语言）实现，允许同一MiniZinc模型无需修改代码即可在多个后端上使用。MiniZinc的一个关键特性是使用全局约束，这极大地简化了建模过程。例如，all\_different约束指定一组变量必须取不同值，替代了众多成对不等式约束。MiniZinc语言结构由四个主要部分组成：决策变量、约束、参数和目标函数（用于优化）或满足目标。MiniZinc还将模型（.mzn文件）与数据实例（.dzn文件）分离，允许一个模型在多个问题实例上重用。

本文建立在两项先前互补工作的基础上：Text2Zinc数据集为这项任务建立了通用基准，以及Text2Model副驾驶为各种LLM方法建立了基线性能。

### 2.2 Text2Zinc数据集

Text2Zinc（Singirikonda等人，2025）引入了一个跨领域数据集，用于在MiniZinc中建模优化和满足问题。它是该研究方向中第一个在求解器和范式无关语言中同时涵盖满足和优化问题的数据集。该数据集汇集了来自多个来源的1,775个问题，包括Nlp4lp（AhmadiTeshnizi等人，2024）、Hakank、ComplexOr（Xiao等人，2023）、LpWp（Ramamonjison等人，2022）、CspLib以及来自Cardinal Operations的问题，涵盖了Mamo和Nl4Opt（Kadıoğlu等人，2024）集合（按类别的完整细分见表1）。其中，110个问题通过手动编写的MiniZinc模型、完整元数据和验证过的解进行了充分验证。对于其余问题（来自IndustryOr、Mamo和Nl4Opt），通过原始来源可获得验证用的真实目标值。数据集提供了is\_optimization、is\_satisfaction、has\_verified\_obj、has\_verified\_mzn、has\_dzn来区分这些属性。

### 2.3 Text2Model副驾驶

Text2Model（Kadıoğlu等人，2026）介绍了一套使用前沿LLM进行文本到模型翻译的副驾驶。它在Text2Zinc数据集上评估了多种复杂度不同的策略，包括零样本提示、思维链推理、知识图谱表示、基于语法的编码和智能体方法。一个关键观察是，即使采用复杂提示策略的前沿LLM，对于组合建模来说也还不是即插即用的技术。

## 3 Learn2Zinc：小语言模型微调

促使本工作的关键见解如下。在数百个Text2Zinc实例上运行多个Text2Model副驾驶会产生大量MiniZinc模型，即使这些MiniZinc模型并非手动编写。虽然生成很简单，但关键优势来自于验证循环：输出可以通过优化问题的已知目标值进行验证，满足问题的可行性也可以断言。这就产生了一个大规模的已验证⟨文本,模型⟩对池，使得微调成为可能。在本文中，我们超越了依赖大型前沿模型生成约束模型的做法，研究针对性的微调能否教会小语言模型（0.6B–20B参数）生成MiniZinc代码。至关重要的是，这项工作需要设计一个微调数据集。

我们的微调数据集从Text2Zinc中已验证的MiniZinc解开始。此外，我们利用Or-Instruct数据集（Huang等人，2024）⁵⁵⁵我们感谢Or-Instruct数据集的创建者对社区的宝贵贡献。提取样本。Or-Instruct数据集包含用Python编写的Copt模型的优化问题。给定这些问题描述、它们的Copt模型和已验证的目标值，我们使用GPT-5.2生成从Copt到MiniZinc的翻译。当且仅当MiniZinc输出与已知目标匹配时，我们才将结果添加到微调数据集中。如表1所示，当Text2Zinc和Or-Instruct的MiniZinc模型合并时，它们共同覆盖了2,208个独特问题。重要的是，实例可能关联由不同Text2Model副驾驶策略生成的替代MiniZinc模型。总体而言，这产生了8,014个用于微调小语言模型的指令调优⟨文本,模型⟩对。

**表1：按来源的独特问题实例分布。来自Text2Zinc的问题通过Text2Model副驾驶策略针对已知目标进行了验证。Or-Instruct问题通过GPT-5.2从Python编写的Copt模型翻译为MiniZinc。**

| 数据集来源 | 实例数 | 百分比 |
| --- | --- | --- |
| Orlm (Huang et al., 2024) Or-Instruct-3K | 1,351 | 61.2% |
| Text2Zinc (Singirikonda et al., 2025) Mamo | 604 | 27.4% |
| Nl4Opt | 200 | 9.1% |
| Nlp4Lp | 30 | 1.4% |
| Hakank | 10 | 0.5% |
| ComplexOr | 5 | 0.2% |
| LpWp | 5 | 0.2% |
| CspLib | 3 | 0.1% |
| **总计** | **2,208** | **100%** |

## 4 Learn2Zinc：微调方法

我们的微调方法包括结合不同参数规模的小语言模型和不同的微调数据集。我们考虑代码生成微调和纠错微调来教授SLM MiniZinc语法（§5）。

### 4.1 小语言模型（SLMs）

我们考虑四个不同系列的小语言模型（SLMs）：Qwen、LLaMa、Gemma和GPT。具体来说，我们微调了五个不同变体以覆盖不同参数规模：Qwen3-0.6B（最小的，用于测试能力下限）、LLaMA-3.2-1B和LLaMA-3.2-3B、Gemma-2-9B以及GPT-OSS-20B（最大参数规模）。

### 4.2 数据集与设置

我们考虑三个不同的微调指令数据集，以建立基线、思维链和混合策略。

#### Learn2Zinc-Base。
我们获得8,014个⟨文本,模型⟩对实例，如§4所述。

#### Learn2Zinc-CoT（思维链）。
我们取基线数据集中的⟨文本,模型⟩对，并提示推理模型GPT4o从问题文本到约束模型生成推理链，并识别变量、参数、约束、目标。因此，该数据集也包含8,014个⟨文本,推理,模型⟩对。

#### Learn2Zinc-Base+CoT。
我们将Learn2Zinc-Base和Learn2Zinc-CoT的示例合并，得到16,028个对。在附录A中，我们展示了基线和CoT对的示例。注意CoT版本如何在问题描述和约束模型之间引入推理链作为中介。

在我们的实验中，我们在三个不同的微调数据集上微调了五个不同的SLM。训练超参数详见附录表10。我们对所有模型采用低秩适应（LoRA）并配合8位量化（GPT-OSS-20B采用4位），以适应单个A100 GPU。我们选择LoRA而非全微调有两个原因。首先，我们的微调数据集相对较小，基数据集仅包含8,014个实例。在这种规模下，全微调容易过拟合，并且相比参数高效替代方案收益有限。其次，LoRA显著降低了内存和计算需求，使我们能够在单个GPU上微调从0.6B到20B参数的模型，而全微调则不可行。在参数高效微调（PEFT）方法中，LoRA已经成熟且被广泛采用，在任务适应和训练效率之间提供了良好的平衡，使其成为我们实验设置的合适选择。

| 模型 | 策略 | 执行准确率 (%) | 解准确率 (%) |
| --- | --- | --- | --- |
| Qwen3-0.6B | 原始-8bit | 0.0 | 0.0 |
| | Learn2Zinc-Base | 51.0 | 9.0 |
| | Learn2Zinc-CoT | 44.0 | 10.0 |
| | Learn2Zinc-Base+CoT | 51.0 | 12.0 |
| | Learn2Zinc-Augmented | 64.0 | 13.0 |
| LLaMA-3.2-1B | 原始-8bit | 0.0 | 0.0 |
| | Learn2Zinc-Base | 44.0 | 4.0 |
| | Learn2Zinc-CoT | 22.0 | 1.0 |
| | Learn2Zinc-Base+CoT | 46.0 | 4.0 |
| | Learn2Zinc-Augmented | 57.0 | 8.0 |
| LLaMA-3.2-3B | 原始-8bit | 0.0 | 0.0 |
| | Learn2Zinc-Base | 62.0 | 10.0 |
| | Learn2Zinc-CoT | 47.0 | ... |