Tadashi: 用于保证正确性的 AI 自动代码生成

自动生成代码的框架和领域特定语言传统上依赖于人类专家来实现严格的方法，以确保代码转换的合法性。最近，机器学习（ML）在为特定硬件目标生成优化代码方面获得了越来越大的关注。然而，机器学习方法——特别是黑箱神经网络——对它们所产生的转换的正确性和合法性没有任何保证。为解决这一差距，我们引入了 Tadashi，一个端到端系统，利用多边形模型支持研究人员为 ML 基于代码生成精选关键数据集。Tadashi 提供了一个端到端系统，能够在保证可靠性和实用性的同时，对多边形日程进行候选转换的应用、验证和评估。我们形式化地证明了 Tadashi 保证生成转换的合法性，展示了其低运行时开销，并展示了其广泛的适用性。Tadashi 项目地址为 https://github.com/vatai/tadashi/。