Fugu-MT 論文翻訳(概要): Automatic Textbook Formalization

論文の概要: Automatic Textbook Formalization

arxiv url: http://arxiv.org/abs/2604.03071v1
Date: Fri, 03 Apr 2026 14:51:01 GMT
ステータス: 翻訳完了
システム内更新日: 2026-04-06 17:20:24.499634
Title: Automatic Textbook Formalization
Title（参考訳）: テキストの自動形式化
Authors: Fabian Gloeckle, Ahmad Rammal, Charles Arnal, Remi Munos, Vivien Cabannes, Gabriel Synnaeve, Amaury Hayat,
Abstract要約: 本稿では,自動AIシステムが500ページ以上の大学院レベルの代数をリーンに変換する教科書を定式化するケーススタディを提案する。結果として得られる形式化は、教科書の形式化スケールと習熟度における新しいマイルストーンである。コード、結果のLeanコードベース、およびサイドバイサイドの青写真Webサイトをオープンソースにしています。
参考スコア（独自算出の注目度）: 30.393353492942527
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization represents a new milestone in textbook formalization scale and proficiency, moving from early results in undergraduate topology and restructuring of existing library content to a full standalone formalization of a graduate textbook. The formalization comprises 130K lines of code and 5900 Lean declarations and was conducted within one week by a total of 30K Claude 4.5 Opus agents collaborating in parallel on a shared code base via version control, simultaneously setting a record in multi-agent software engineering with usable results. The inference cost matches or undercuts what we estimate as the salaries required for a team of human experts, and we expect there is still the potential for large efficiencies to be made without the need for better models. We make our code, the resulting Lean code base and a side-by-side blueprint website available open-source.
Abstract（参考訳）: 本稿では,自動AIシステムが500ページ以上の代数的コンビネータの教科書をLeanに形式化するケーススタディを提案する。結果として得られた形式化は、教科書の形式化スケールと習熟度における新たなマイルストーンであり、学部のトポロジの初期の結果から、既存の図書館内容の再構成から、大学院の教科書の完全なスタンドアロンの形式化へと移行した。フォーマル化は130K行のコードと5900のリーン宣言で構成され、1週間以内に30K Claude 4.5 Opusエージェントがバージョン管理を通じて共有コードベース上で共同作業を行い、同時にマルチエージェントソフトウェアエンジニアリングにおける記録を使用可能な結果で設定した。推論コストは、人間の専門家のチームに必要な給与として見積もっているものと一致または下降します。コード、結果のLeanコードベース、およびサイドバイサイドの青写真Webサイトをオープンソースにしています。

関連論文リスト

IQuest-Coder-V1 Technical Report [56.045533451719905]
IQuest-Coder-V1 シリーズ-(7B/14B/40B/40B-Loop) は、新しいコード大言語モデル(LLM)のファミリーである。 IQuest-Coder-V1は、コードインテリジェンスの重要な次元にわたる競合モデルの最先端のパフォーマンスを達成する。
論文参考訳（メタデータ） (2026-03-17T16:15:31Z)
Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
論文参考訳（メタデータ） (2026-02-02T16:24:53Z)
DeepCode: Open Agentic Coding [11.7906174865581]
DeepCodeは、ドキュメントからコードへの合成のための完全に自律的なフレームワークである。有限のコンテキスト予算の下でタスク関連信号を最大化する4つの情報操作を編成する。 PaperBenchベンチマークの大規模な評価は、DeepCodeが最先端のパフォーマンスを達成したことを示している。
論文参考訳（メタデータ） (2025-12-08T16:07:13Z)
From Code Foundation Models to Agents and Applications: A Practical Guide to Code Intelligence [150.3696990310269]
大規模言語モデル(LLM)は、自然言語記述を直接関数コードに変換することによって、自動ソフトウェア開発を変革した。コードLLMに関する総合的な合成と実践的ガイド(一連の解析および探索実験)を提供する。一般LLM(GPT-4, Claude, LLaMA)とコード特殊化LLM(StarCoder, Code LLaMA, DeepSeek-Coder, QwenCoder)のコード機能の解析を行う。
論文参考訳（メタデータ） (2025-11-23T17:09:34Z)
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)
Paper2Code: Automating Code Generation from Scientific Papers in Machine Learning [70.04746094652653]
機械学習論文を機能コードリポジトリに変換するフレームワークであるPaperCoderを紹介した。 PaperCoderは3つの段階で動作する。計画、図によるシステムアーキテクチャの設計、ファイル依存の特定、構成ファイルの生成である。次に、モデルベースおよび人的評価の両方に基づいて、機械学習論文からコード実装を生成するPaperCoderを評価する。
論文参考訳（メタデータ） (2025-04-24T01:57:01Z)
UnitCoder: Scalable Iterative Code Synthesis with Unit Test Guidance [65.01483640267885]
大きな言語モデル(LLM)は、様々なタスクにおいて顕著な能力を示してきたが、コード生成は依然として大きな課題である。私たちは、モデル生成ユニットテストを活用してコード生成プロセスのガイドと検証を行う、システマティックパイプラインであるUnitCoderを紹介します。我々の研究は、モデル生成単体テストを利用して、事前学習コーパスから高品質なコードデータの合成を誘導するスケーラブルなアプローチを提案する。
論文参考訳（メタデータ） (2025-02-17T05:37:02Z)
Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。このモデルは、微粒な類似性計算法と再ランクモジュールを応用した、対照的な学習フレームワークで学習される。実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。
論文参考訳（メタデータ） (2025-01-21T06:32:25Z)

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

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