Fugu-MT 論文翻訳(概要): Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations

論文の概要: Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations

arxiv url: http://arxiv.org/abs/2611.02843v1
Date: Mon, 02 Nov 2026 09:45:31 GMT
ステータス: 翻訳完了
システム内更新日: 2026-11-06 14:55:26.611234
Title: Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations
Title（参考訳）: 数学基礎形式化エージェント : 数学的基礎を形式化する汎用的アプローチ
Abstract要約: 本稿では,複数の数学的領域にまたがる形式化タスクを支援する汎用知的エージェントであるMath Foundation Formalization Agent (MFF-Agent)を提案する。エージェントは、大規模言語モデルの推論能力と、Rocq証明アシスタントの形式的検証能力を統合する。単一の数学的理論に焦点を当てたアプローチとは異なり、エージェントはモース-ケリー公理集合論を含むケーススタディを通して検証される。
参考スコア（独自算出の注目度）: 6.880596807191613
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning. With the development of large language models (LLMs) and interactive theorem provers, intelligent agents offer a promising approach to automating the formalization of mathematical theories. This paper presents the Math Foundation Formalization Agent (MFF-Agent), a general-purpose intelligent agent designed to support formalization tasks across multiple mathematical domains. The agent integrates the reasoning capabilities of large language models with the formal verification capabilities of the Rocq proof assistant. It incorporates task classification, tool-assisted execution, verification feedback, and state-based task management to support the generation, refinement, and verification of formal proofs. Unlike an approach focused on a single mathematical theory, the agent is examined through case studies involving Morse--Kelley axiomatic set theory (MK), real numbers, propositional logic, and equivalences of the axiom of choice. These cases investigate its applicability across mathematical foundations and distinguish source-level completion, interactive verification, and reproducible compilation. The results demonstrate the feasibility of a unified operational framework for heterogeneous foundation-level tasks and clarify the gap between such a framework and a fully integrated mathematical foundation.
Abstract（参考訳）: 数学的形式化は、数学的推論のための厳密でマシン検証可能な基礎を確立する上で重要な役割を果たしている。大規模言語モデル(LLM)と対話的定理証明器の開発により、インテリジェントエージェントは数学的理論の形式化を自動化するための有望なアプローチを提供する。本稿では,複数の数学的領域にまたがる形式化タスクを支援する汎用知的エージェントであるMath Foundation Formalization Agent (MFF-Agent)を提案する。エージェントは、大規模言語モデルの推論能力と、Rocq証明アシスタントの形式的検証能力を統合する。タスク分類、ツール支援実行、検証フィードバック、および状態ベースのタスク管理を組み込んで、形式的証明の生成、洗練、検証をサポートする。単一の数学的理論に焦点を当てたアプローチとは異なり、エージェントはモース-ケリー公理集合論(MK)、実数、命題論理、選択公理の同値性を含むケーススタディを通して検証される。これらのケースは、数学的基礎を越えて適用可能性を調査し、ソースレベルの補完、インタラクティブな検証、再現可能なコンパイルを区別する。これらの結果から,不均一な基礎レベルのタスクに対する統一的な運用フレームワークの実現可能性を示し,そのようなフレームワークと完全に統合された数学的基礎とのギャップを明らかにした。

関連論文リスト

From Atomic to Agentic: Towards Interpretable Evaluation of LLMs' Agentic Mathematical Capabilities [103.60384544335072]
大規模言語モデル(LLM)は、エンドツーエンドの数学的推論からエージェントインテリジェンスの統合へと進化している。本フレームワークは,問題解決エージェントの挙動を,再利用可能な数学的原子能力の構造化された分類法と整合させる。実験により、同様のエンドツーエンドの精度を持つモデルでは、エージェント能力プロファイルが著しく異なることが判明した。
論文参考訳（メタデータ） (2026-08-27T10:52:06Z)
MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文参考訳（メタデータ） (2026-07-16T05:22:40Z)
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
論文参考訳（メタデータ） (2026-07-08T17:46:36Z)
MechMath Agent Team: LLM Driven Agents for Mathematical Research [17.23955320294417]
MechMath Agent Team (MMAT) は、数学研究の全サイクルを通して共同パイロットとして機能するように設計された大規模言語モデル駆動エージェントである。我々は、システムの責任をコントロール、実行、拡張プレーンに分離する三部構成のハーネスアーキテクチャを設計する。我々は、数論、代数的複素性理論、微分代数、作用素代数、不等式における開問題に関するMMATを評価する。
論文参考訳（メタデータ） (2026-07-05T16:37:40Z)
Automated Conjecture Resolution with Formal Verification [21.763678203045973]
本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
論文参考訳（メタデータ） (2026-04-04T16:35:16Z)
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics [1.2978846076301875]
Ax-Proverは、リーンにおける自動定理証明のためのマルチエージェントシステムである。様々な科学的領域にまたがる問題を解決し、自律的または協調的に人間の専門家と操作することができる。我々は,2つの公的な数学ベンチマークと,抽象代数学と量子論の分野において導入される2つのリーンベンチマークにおいて,フロンティア LLM と特殊証明モデルに対するアプローチをベンチマークする。
論文参考訳（メタデータ） (2025-10-14T17:57:04Z)
DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文参考訳（メタデータ） (2025-05-29T17:59:39Z)
LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
論文参考訳（メタデータ） (2024-10-08T17:11:24Z)
math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
論文参考訳（メタデータ） (2023-10-25T23:54:04Z)

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

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