論文の概要: Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

• arxiv url: http://arxiv.org/abs/2606.31134v2
• Date: Wed, 01 Jul 2026 19:08:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-03 15:16:32.247515
• Title: Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
• Title（参考訳）: 図書館を超えて: 研究数学のオートフォーマル化のためのエージェントフレームワーク
• Abstract要約: 大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。 最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。 汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
• 参考スコア（独自算出の注目度）: 20.90238876313568
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .
• Abstract（参考訳）: 大規模言語モデル(LLM)は数学的推論において例外的な能力を示したが、人間の検出を避ける微妙な誤りをしばしば生み出す。 Lean 4のようなフォーマルな数学的言語は、機械的証明チェックを提供し、自然言語数学を検証可能なコードに自動変換する自動形式化の必要性を強く動機付けている。 最近の傾向は、標準プログラミングに強く最適化された汎用LLMが、リーンのために明確に調整されたより小さなモデルより優れていることを示している。 このシフトを生かして、汎用的なLLMを用いたエージェントオートフォーマル化フレームワークを導入する。 私たちのシステムの中核は、研究レベルの数学に適したマルチエージェントパイプラインを管理するオーケストレータです。 最先端の研究は、Mathlibのような既存のライブラリの範囲外の概念に頻繁に依存するため、我々のシステムは、必要となる型定義を動的に拡張し、プライマリ定理を定式化する前に、新しい補助レンマ手法によってそれらを検証する。 私たちはPatnamBenchにアプローチを適用し、32の問題をランダムにサンプルしたマシンチェックのリーン証明を作成しました。 さらに, ACM Symposium on Theory of Computing (STOC) acrossing combinatorics, communication complexity, mechanism design, and learning theory, successfully formalization their main theorems and valid of the generated formalizations with human expert, and all 5 we also formalize the proofs along the statement, and noted they are not no axioms beyond Lean's kernel。 公式化はすべてhttps://beyondthelibrary.github.io/formal_arxiv で利用可能です。

関連論文リスト

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
  論文  参考訳（メタデータ） (2026-07-16T05:22:40Z)
• Multi-agent Autoformalization of Tensor Network Theory [0.21847754147782886]
  我々は、専門的な大規模言語モデルエージェントのチームを構築し、理論物理学における研究レベルの形式化のためのエージェント駆動ワークフローを提示する。 エージェントは、構造化された数学的青写真と定期的な人間のレビューを通して調整し、完全な形式化を自律的にオーケストレーションし実行した。 いくつかの声明では、エージェントは標準的な文献には含まれない新しい証明ルートを探索することができた。
  論文  参考訳（メタデータ） (2026-07-08T18:43:33Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。 この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
  論文  参考訳（メタデータ） (2026-07-08T17:46:36Z)
• 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)
• 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)

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

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