用AI团队自动形式化张量网络理论，验证了矩阵乘积态基本定理。
Multi-agent Autoformalization of Tensor Network Theory
- 组建专业AI代理团队，按数学蓝图协作完成理论形式化。
- 自主探索出文献外的新证明路径，构建全新张量网络库。
- 适合对形式化推理、量子物理与AI协同研究者参考。
我们构建了一支由专业化大语言模型代理组成的团队，提出一种代理驱动的研究级形式化工作流，以矩阵乘积态的基本定理的自动形式化为例进行演示。这些代理通过结构化的数学蓝图和周期性的人工评审进行协调，自主完成了整个形式化过程。对于部分命题，代理探索出了标准文献之外的新证明路径。在此过程中，代理还构建了数学库Mathlib中此前不存在的大量张量网络与量子信息相关库。作为物理应用，形式化还拓展至一维对称保护拓扑相。我们发现大规模自动形式化的关键瓶颈在于保持数学意图的一致性，并对全过程及其中各种细微问题进行了详细研究。代码库已发布为TNLean，配套提供包含若干章节的正式化蓝图文档。
原文摘要 · Abstract (English)
We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration. The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously. For some statements, the agents were able to explore new proof routes that are not part of the standard literature. Along the way the agents produced extensive tensor-network and quantum-information libraries not previously available in Mathlib, Lean's mathematical library. As a physical application, the formalization also extends towards symmetry-protected topological phases in one dimension. We find that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and we provide a detailed study of the full process and various subtleties involved. We release the codebase as the library \href{https://github.com/LionSR/TNLean}{TNLean}, together with a \nChapters{}-chapter \href{https://lionsr.github.io/TNLean/blueprint/}{blueprint} of the formalization effort.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。