論文の概要: Multi-agent Autoformalization of Tensor Network Theory
- arxiv url: http://arxiv.org/abs/2607.07857v1
- Date: Wed, 08 Jul 2026 18:43:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-10 14:45:27.322152
- Title: Multi-agent Autoformalization of Tensor Network Theory
- Title（参考訳）: テンソルネットワーク理論のマルチエージェントオートフォーマル化
- Abstract要約: 我々は、専門的な大規模言語モデルエージェントのチームを構築し、理論物理学における研究レベルの形式化のためのエージェント駆動ワークフローを提示する。
エージェントは、構造化された数学的青写真と定期的な人間のレビューを通して調整し、完全な形式化を自律的にオーケストレーションし実行した。
いくつかの声明では、エージェントは標準的な文献には含まれない新しい証明ルートを探索することができた。
- 参考スコア（独自算出の注目度）: 0.21847754147782886
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 専門的な大規模言語モデルエージェントのチームを構築し、理論物理学における研究レベルの形式化のためのエージェント駆動ワークフローを示し、実証として行列積状態の基本定理の自己形式化を行う。
エージェントは、構造化された数学的青写真と定期的な人間のレビューを通して調整され、完全な形式化を自律的にオーケストレーションし実行した。
いくつかの声明では、エージェントは標準的な文献には含まれない新しい証明ルートを探索することができた。
その過程でエージェントは、リーンの数学的ライブラリであるMathlibで以前は利用できなかった広範なテンソル・ネットワークと量子情報ライブラリを作成した。
物理的応用として、形式化は1次元の対称性で保護された位相相にも拡張される。
大規模自己形式化の主なボトルネックは、数学的意図を強制することであり、我々は、その完全なプロセスと関連する様々な微妙さについて詳細に研究している。
フォーマル化作業の成果として,ライブラリである \href{https://github.com/LionSR/TNLean}{TNLean} と \nChapters{}-chapter \href{https://lionsr.github.io/TNLean/blueprint/}{blueprint} としてコードベースをリリースしています。
関連論文リスト
- Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。
最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。
汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
論文 参考訳（メタデータ） (2026-06-30T05:05:03Z) - Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance [0.3624700141426058]
コーディングエージェントはLean 4で高度な数学教科書全体を形式化できます。
本稿では,コンパイラを超えてエージェント生成形式の品質を評価するためのフレームワークを提案する。
以上の結果から,コンパイルベースのメトリクスは形式化品質を大幅に上回っていることが示唆された。
論文 参考訳（メタデータ） (2026-06-12T00:45:42Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean [7.11696910077237]
FormalScienceは、人為的なエージェントパイプラインで、テキストシンタクティックに正確で、テキスト的に整列された、低い経済コストに対する非公式な推論の形式的証明を生成する。
我々は、Lean4の公式表現とともに200の物理問題と解(主に量子力学と電磁磁性)のデータセットであるFormalPhysicsを構築した。
我々は、ゼロショットプロンプト、エラーフィードバックによる自己抑制、新しいマルチステージエージェントアプローチを通じて、データセット上のステートメントの自動形式化タスクに基づいて、オープンソースモデルとプロプライエタリシステムを評価する。
論文 参考訳（メタデータ） (2026-04-24T20:47:22Z) - Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。
エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。
この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
論文 参考訳（メタデータ） (2026-02-02T16:24:53Z) - MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。
さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
論文 参考訳（メタデータ） (2026-01-30T15:24:42Z) - Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics [25.762535169301984]
我々はClude CodeとNumina-Lean-MCPを組み合わせたNumina-Lean-Agentを導入し、リーンとの自律的なインタラクションを可能にします。
Claude Opus 4.5 をベースモデルとして、Numina-Lean-Agent はPutnam 2025 (12 / 12) の全ての問題を解決する。
論文 参考訳（メタデータ） (2026-01-20T14:51:45Z) - LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。
LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。
これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
論文 参考訳（メタデータ） (2024-10-08T17:11:24Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳（メタデータ） (2023-10-12T00:50:24Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。