面向语法引导合成的强化学习与数据生成方法
人工智能
2024-01-08 v2
摘要
程序合成是根据规约自动生成代码的任务。在语法引导合成（SyGuS）中，该规约由语法模板与逻辑公式组合而成，所得结果保证同时满足二者。我们提出了一种由强化学习引导的 SyGuS 算法，该算法使用蒙特卡洛树搜索（MCTS）来搜索候选解空间。我们的算法学习策略函数与价值函数，并结合树的上置信界（upper confidence bound for trees），使其能平衡探索与利用。将机器学习方法应用于语法引导合成的一个常见挑战是训练数据的稀缺。为此，我们提出了一种基于现有可满足性模理论（first-order satisfiability）问题的反统一（anti-unification）自动生成 SyGuS 训练数据的方法，并用其训练我们的 MCTS 策略。我们实现并评估了该方案，结果表明在训练集和测试集上，学习到的策略与价值使合成性能相较基线提升超过 26 个百分点。我们的工具在训练集上优于当前最优工具 cvc5，在测试集上就解决的问题总数而言表现相当（在 cvc5 失败的基准上解决了 23%）。我们公开了数据集，以便将机器学习方法进一步应用于 SyGuS 问题。
引用
@article{arxiv.2307.09564,
title = {Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis},
author = {Julian Parsert and Elizabeth Polgreen},
journal= {arXiv preprint arXiv:2307.09564},
year = {2024}
}