研究札記
面向軟體工程的受約束程式碼生成
實務上區分生成程式碼的文法約束、型別約束、保留邊界與行為層級驗收檢查。
直接回答
在軟體工程工作流程中，受限程式碼生成能保證什麼？
只有約束明確強制執行的屬性。文法約束解碼可保證輸出屬於某套文法；型別感知方法可針對型別有效性；但兩者單獨使用皆無法證明任務正確性、語意等價性、行為保存或編輯局部性。
此項區分為何重要
方法與所宣稱的保證必須採用相同的可觀察邊界。
若未指明受約束的性質，「受限」一詞便不完整。解碼器可以強制遵守語法，型別檢查器可以限制有效的後續內容，編輯器可以保護選定區域，而修復工作流程則可僅接受通過測試的候選方案。這些機制解決的是不同問題。
因此，有效的評估必須使控制機制與所宣稱的保證相互對應。通過剖析器可作為語法方面的相關證據，卻不能證明程式符合要求，亦不能證明編輯範圍以外的行為獲得保留。
實務流程
明確指出所需屬性
判定需求涉及的是文法、型別、API、原始碼局部性、結構不變量、測試，或其他可觀察的契約。
選擇約束施行點
若可行，應在解碼期間施加約束；若相關性質只能於生成後檢查，則採用「提出候選方案並加以驗證」的方法。
維持彼此獨立的驗收檢查
即使解碼器已保證語法或型別，仍須測試任務成功情形與受保護屬性。
報告拒絕與失敗行為
受約束的方法應揭露候選結果遭拒的頻率、有效解是否仍可到達，以及哪些性質尚未檢查。
必須具備的證據
一項主張的可信度，取決於生成或解碼後實際量測的性質所能提供的證據強度。
- 受約束屬性以可觀察的方式陳述。
- 施行機制與生成後檢查有所區分。
- 本文不將語法或型別有效性視為功能正確性。
- 當論述涉及程式碼維持不變時，便直接量測局部性。
- 報告約束失敗、拒絕率與任務成功率。
所連結研究的報告內容
- 連結的階層式潛在表示研究鎖定選定的學習碼，並量測解碼後的剖析率、編輯自由度與多樣性。
- 這是一項可檢視的部分控制實驗，並非對形式文法、型別、語意或行為的保證。
- 對受約束工作流程而言，其價值在於明確的控制介面與嚴謹的量測規範，而非主張鎖定潛在表示可取代形式驗證。
範圍邊界
- 不同約束之間可能互相衝突；更嚴格的限制可能排除有效解答，或降低生成結果的多樣性。
- 生成後測試僅能為其涵蓋的行為提供證據。
- 連結的論文並未評估形式化受約束解碼或儲存庫規模的軟體修復。
主要與鄰近文獻來源
原始方法、量測結果與明列限制，請參閱所連結的論文。
- Inspectable Control for Structure-Preserving Software Regeneration
本站探討階層式潛在表示中可檢視局部控制的主要論文。
- Type-Constrained Code Generation with Language Models
適用於語言模型程式碼生成的型別感知約束。