Tadashi 用数学模型保证机器学习生成代码的正确性，让自动编程更可靠。
Tadashi: Enabling AI-Based Automated Code Generation With Guaranteed Correctness
- 基于多面体模型自动生成并验证代码变换
- 形式化证明生成变换始终合法，运行开销低
- 适合需要高可靠性代码生成的研究者
用于自动代码生成的框架和领域特定语言传统上依赖人工专家实现严格的代码变换合法性保障。近年来，机器学习（ML）在生成针对特定硬件优化的代码方面日益流行。然而，尤其是黑箱神经网络类的ML方法无法保证其生成变换的正确性或合法性。为填补这一空白，我们提出 Tadashi，一个端到端系统，利用多面体模型支持研究人员构建对基于ML的代码生成至关重要的数据集。Tadashi 能够以可靠性和实用性完成对多面体调度中候选变换的生成、验证与评估。我们形式化证明了 Tadashi 保证生成变换的合法性，展示了其低运行时开销，并验证了其广泛适用性。Tadashi 已开源：https://github.com/vatai/tadashi/
原文摘要 · Abstract (English)
Frameworks and domain-specific languages for auto-generating code have traditionally depended on human experts to implement rigorous methods ensuring the legality of code transformations. Recently, machine learning (ML) has gained traction for generating code optimized for specific hardware targets. However, ML approaches-particularly black-box neural networks-offer no guarantees on the correctness or legality of the transformations they produce. To address this gap, we introduce Tadashi, an end-to-end system that leverages the polyhedral model to support researchers in curating datasets critical for ML-based code generation. Tadashi provides an end-to-end system capable of applying, verifying, and evaluating candidate transformations on polyhedral schedules with both reliability and practicality. We formally prove that Tadashi guarantees the legality of generated transformations, demonstrate its low runtime overhead, and showcase its broad applicability. Tadashi available at https://github.com/vatai/tadashi/.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。