論文の概要: Formalizing Mathematics at Scale

• arxiv url: http://arxiv.org/abs/2605.29955v1
• Date: Thu, 28 May 2026 14:00:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-30 02:45:56.373497
• Title: Formalizing Mathematics at Scale
• Title（参考訳）: 大規模数学の形式化
• Authors: Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat, Julia Kempe, Remi Munos, Charles Arnal, Vivien Cabannes,
• Abstract要約: AutoformBotは、正式な検証ツール、依存性対応タスクスケジューリング、協調バージョン管理を備えた数千のLLMエージェントをオーケストレーションする。 Atlasは45,000以上のLean 4宣言と5万行のコードからなる検証済みのライブラリです。 結果は,大学院レベルの数学の中核的内容の大規模化は,現在,経済的かつ技術的に実現可能であることを示唆している。
• 参考スコア（独自算出の注目度）: 26.679968935283558
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.
• Abstract（参考訳）: 私たちは、Lean 4.0でAutoformalized Textbook Library At Scale(Atlas)を構築するマルチエージェントシステムであるAutoformBotを紹介します。 AutoformBotは、公式の検証ツール、依存性対応タスクスケジューリング、共同バージョン管理を備えた数千のLLMエージェントを編成し、非公式の教科書の散文を機械チェックされた定義と証明に翻訳する。 我々は、分析、代数、トポロジ、コンビネータ、確率にまたがる26のオープンアクセス教科書のコーパスに適用し、45,000以上のLean 4宣言と5万行のコードからなる検証済みライブラリAtlasを作成します。 アーティファクトは2つリリースします。 (i)オープンソースのマルチエージェントフレームワークAutoformBot (ii)Atlasは、結果として得られる形式的なライブラリである。 以上の結果から,大学院レベルの数学の中核的内容の大規模化は,現在,経済的かつ技術的に実現可能であることが示唆された。 これにより、人間と機械が生成した数学を研究レベルで自動検証する扉が開ける。

関連論文リスト

• Automatic Textbook Formalization [30.393353492942527]
  本稿では,自動AIシステムが500ページ以上の大学院レベルの代数をリーンに変換する教科書を定式化するケーススタディを提案する。 結果として得られる形式化は、教科書の形式化スケールと習熟度における新しいマイルストーンである。 コード、結果のLeanコードベース、およびサイドバイサイドの青写真Webサイトをオープンソースにしています。
  論文  参考訳（メタデータ） (2026-04-03T14:51:01Z)
• Automating Skill Acquisition through Large-Scale Mining of Open-Source Agentic Repositories: A Framework for Multi-Agent Procedural Knowledge Extraction [20.467661664708086]
  本報告では,オープンソースリポジトリのマイニングによる高品質エージェントスキルの自動獲得の枠組みについて検討する。 我々は,TheoremExplainAgentやCode2Videoなどの最先端システムから,可視化と教育能力の抽出に重点を置いている。 エージェントリポジトリからの体系的抽出と厳密なセキュリティガバナンスと多次元評価指標を組み合わせることで、手続き的知識のスケーラブルな獲得が可能になることを実証する。
  論文  参考訳（メタデータ） (2026-03-12T11:10:13Z)
• MerLean: An Agentic Framework for Autoformalization in Quantum Computation [0.0]
  本稿では,量子計算におけるオートフォーマル化のための完全に自動化されたフレームワークであるMerLeanを紹介する。 MerLeanはLaLeanソースファイルからステートメントを抽出し、Mathlib上に構築された検証済みのLean4コードに形式化し、結果を人間可読なLaLean宣言に変換してセマンティックレビューを行う。 我々はMerLeanを114のステートメントから2,050のリーンステートメントを生成する3つの理論量子コンピューティング論文で評価した。
  論文  参考訳（メタデータ） (2026-02-18T15:54:32Z)
• LeMat-Synth: a multi-modal toolbox to curate broad synthesis procedure databases from scientific literature [60.879220305044726]
  本稿では,大規模言語モデル (LLM) と視覚言語モデル (VLM) を用いて合成手順と性能データを自動抽出・整理するマルチモーダルツールボックスを提案する。 LeMat-Synth (v 1.0):35種類の合成法と16種類の材料クラスにまたがる合成手順を含むデータセット。 我々は,新しいコーパスと合成ドメインへのコミュニティ主導の拡張をサポートするために設計された,モジュール形式のオープンソースライブラリをリリースする。
  論文  参考訳（メタデータ） (2025-10-28T17:58:18Z)
• TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition [9.593530910909363]
  TopoAlignは、広く利用可能なコードリポジトリをMath LLMのトレーニングリソースとしてアンロックするフレームワークである。 TopoAlignはコードをdocstring、main関数、Dependency関数に分解し、これらのコンポーネントを形式的なステートメントを構造的にミラーするアナログに再組み立てする。 我々は、DeepSeek-MathとHeraldの2つの最先端モデルをトレーニングし、minif2f、Patnam、ProofNetベンチマークで評価する。
  論文  参考訳（メタデータ） (2025-10-13T21:09:36Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• AutoAct: Automatic Agent Learning from Scratch for QA via Self-Planning [54.47116888545878]
  AutoActはQAのための自動エージェント学習フレームワークである。 大規模アノテートデータやクローズドソースモデルからの合成計画軌道は依存していない。
  論文  参考訳（メタデータ） (2024-01-10T16:57:24Z)
• LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
  LILOは、反復的に合成、圧縮、文書化を行う、ニューロシンボリックなフレームワークである。 LILOは、LLM誘導プログラム合成と、Stitchから自動化された最近のアルゴリズムの進歩を組み合わせたものである。 LILOのシンセサイザーが学習した抽象化を解釈し、デプロイするのを手助けすることで、AutoDocがパフォーマンスを向上させることが分かりました。
  論文  参考訳（メタデータ） (2023-10-30T17:55:02Z)
• MLFMF: Data Sets for Machine Learning for Mathematical Formalization [0.18416014644193068]
  MLFMF(MLFMF)は、証明アシスタントを用いた数学の形式化を支援するために使用されるベンチマークシステムのためのデータセットの集合である。 各データセットは、AgdaやLeanの証明アシスタントで書かれた形式化された数学のライブラリから導かれる。 合計25万ドル以上のエントリーがあり、これは現在、機械学習可能な形式における公式な数学的知識のコレクションとして最大である。
  論文  参考訳（メタデータ） (2023-10-24T17:00:00Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。