中文

张量网络理论的多智能体自动形式化

量子物理 2026-07-08 v1 人工智能
作者: Sirui Lu , Erickson Tjoa , J. Ignacio Cirac
在 arXiv 上查看 ↗ PDF ↗

摘要

我们组建了一个由专业大型语言模型智能体组成的团队，并提出了一种用于理论物理研究级形式化的智能体驱动工作流程，以矩阵乘积态基本定理的自动形式化作为演示。这些智能体通过结构化的数学蓝图和定期的人工审查进行协调，自主地编排并执行了完整的形式化过程。对于某些陈述，智能体能够探索标准文献中不包含的新证明路径。在此过程中，智能体生成了大量以前在 Mathlib（Lean 的数学库）中不可用的张量网络和量子信息库。作为一个物理应用，该形式化还扩展到了一维对称保护拓扑相。我们发现，大规模自动形式化的主要瓶颈是强制执行数学意图，我们提供了对完整过程和涉及的各种细微差别的详细研究。我们将代码库作为库 \href{https://github.com/LionSR/TNLean}{TNLean} 发布，并附有形式化工作的 \nChapters{}-章 \href{https://lionsr.github.io/TNLean/blueprint/}{蓝图}。

关键词

自动形式化 大型语言模型 多智能体系统 张量网络 矩阵乘积态 Lean 定理证明器 理论物理

引用

@article{arxiv.2607.07857,
  title  = {Multi-agent Autoformalization of Tensor Network Theory},
  author = {Sirui Lu and Erickson Tjoa and J. Ignacio Cirac},
  journal= {arXiv preprint arXiv:2607.07857},
  year   = {2026}
}

备注

5+2+33 pages; 3+3+11 figures; 6 tables; An accompanying blueprint document is available at https://lionsr.github.io/TNLean/blueprint-ch01-12.pdf