学习如何构建形式化问题：通过渐进式优化与验证实现 AI 基础设施的智能体驱动软硬件协同设计

AI 基础设施，即用于训练和服务 AI 模型的芯片与软件，是分层设计的。分层使系统易于管理，但也会限定优化器能够考虑的选择。那些需要芯片及其软件协同改变才能实现的收益，在优化开始之前就被排除在外：形式化问题没有将它们纳入。语言模型智能体使重新审视这些边界成为可能，但智能体提出的方案本身无法证明设计是正确的或最优的。我们提出 Formulaic，这是一种划分工作流程的方法：智能体编写形式化问题，数学求解器在其中进行优化，而验证与测量则检查其假设和结果。智能体逐步细化问题，从计算图一直推进到芯片。每一步都是一个模板：一类程序，以及保证其正确性的条件。Wall relaxation 通过对约束软件的硬件限制进行定价来搜索芯片。本文通过彼此独立的研究迈出了第一步，而非进行一次端到端运行。在 NVIDIA GB10 上，智能体编写的模板运行完整的 Qwen3-8B 层时，比 SGLang 快 $1.075\times$。在模拟的 Ventus GPU 研究中，协同设计将 Qwen2.5-0.5B 在最差场景下的周期数降至参考值的 0.428，而仅进行软件优化时为 0.934。在一个五步 GEMM 细化链中，复用证明使检查速度提升了 $2.51\times$。