Jul, 2019

基于约束的类型导向程序合成

PDF
TL;DR使用基于约束的类型推断技术探索了一种类型导向的程序综合方法，以更有效地综合多态代码，并解决建立在多态上的高级类型功能，如 GADTs。辅以我们在 Haskell 编程语言的原型工具 Scythe 中实现的这些技术，并反思我们的初步使用经验。
发现论文，激发创造
  • 多态细化类型的程序合成

    提出了一种基于细化类型的递归函数合成方法，支持自动验证和程序细节拆分，实现了比现有方案更高效和易用的程序合成工具。

    Oct, 2015

  • HOTGP -- 高阶类型遗传规划

    本文介绍了一种新的基于 Haskell 的基因编程算法 HOTGP，它利用规约的数据类型来约束搜索空间，更好地合成类型良好的纯函数编程。经验结果表明，与其他六种算法相比，HOTGP 在综合正确程序的能力上更为优异。

    Apr, 2023

  • OptTyper：通过优化逻辑约束和自然约束进行概率类型推断

    该研究提出了一种概率类型推理框架，在 TypeScript 文件中预测缺失的类型。该框架将来自类型系统的逻辑约束与来自命名约定的深度学习模型提取的自然约束相结合，优于先前使用单一信息的模型。

    Apr, 2020

  • 增强数据流分析的学习类型推断

    CodeTIDAL5 是一种基于 Transformer 的模型，用于可靠地预测类型注释，并从程序的代码属性图中提取使用片段，其在 ManyTypes4TypeScript 基准测试上优于当前最先进的神经类型推理系统 7.85％，总体准确率达到 71.27％。

    Oct, 2023

  • 使用抽象细化进行程序合成

    通过使用抽象语义和基于树自动机的迭代精化方法，我们提出了一种高效的程式合成方法，并在字符串和矩阵转换领域中取得了比现有技术更好的结果。

    Oct, 2017

  • 学习推理程序草图

    本文介绍一种用于程序自动合成的方法，通过结合模式识别和显式推理来解决这些复杂的编程问题，同时使用新颖的中间表示和训练算法，使程序合成系统能够自学，从而在简单的英文描述编程问题数据集上取得了最先进的性能表现。

    Feb, 2019

  • 基于强化学习的语法引导综合

    在这项研究中，我们将通用 SyGuS 问题作为树搜索框架，并提出了一种基于蒙特卡洛树搜索 (MCTS) 的增强学习引导合成算法。我们的算法结合了学习到的策略和值函数，以及平衡探索和利用的树上置信上界。我们还介绍了一种基于现有一阶可满足性问题的反合一方法自动生成 SyGuS 的训练数据。通过这些成果，我们的工具在训练和测试集中相比基准枚举算法提高了 26 个百分点，超过了 1 CVC5 等最先进工具的表现，同时我们还公开了我们的数据集以便于进一步应用机器学习方法解决 SyGuS 问题。

    Jul, 2023

  • 函数式编码构建遗传编程

    研究了一种基于遗传编程的编程合成方法，利用反射和一级规范来支持进化可能使用任意数据类型、多态和现有代码库中的函数的程序，使用 Hindley-Milner 类型系统可以演化类型安全的程序，并将性能与其他现代遗传编程方法进行比较。

    Jun, 2022

  • 计算机程序合成的依赖关系量化公式模 Theory

    研究了没有语言文法限制的综合技术，证明它可以被约化为 DQF 问题，通过 DQF 求解来设计综合程序并且克服了基于文法的综合技术的限制，实现了更好的性能。

    May, 2021

  • 从静态分析引导的示例中综合关键程序

    我们提出了一种新颖的算法，该算法合成初级编程课程的命令式程序，基于枚举程序合成和静态分析相结合的关键思想，我们的算法在平均 6.6 秒内能够解决基准问题。

    Feb, 2017