Fugu-MT 論文翻訳(概要): AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities

論文の概要: AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities

arxiv url: http://arxiv.org/abs/2606.26442v1
Date: Wed, 24 Jun 2026 23:09:49 GMT
ステータス: 翻訳完了
システム内更新日: 2026-06-26 18:46:32.097973
Title: AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
Title（参考訳）: AXLE: 実用性を証明するリーン4理論のためのクラウドインフラストラクチャ
Abstract要約: AXLEはLean 4の証明操作、抽出、検証のためのクラウドサービスである。これまでに5億以上のリクエストを処理し、Axiom Mathの証明活動の基盤となっている。
参考スコア（独自算出の注目度）: 1.7375804203462168
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present AXLE (Axiom Lean Engine), a cloud service for Lean 4 proof manipulation, extraction, and verification. Recent progress in AI for mathematics -- reinforcement learning pipelines, agentic proving workflows, dataset curation -- demands Lean 4 tooling that scales to millions of requests while remaining correct and robust; existing infrastructure offers parallel compilation but not scalable proof verification, higher-level proof manipulation, multi-version support, or per-request isolation at the throughput modern AI workflows require. AXLE provides 14 Lean 4 metaprogramming tools spanning strict proof verification, declaration metadata extraction, semantic source manipulation, deterministic proof repair and simplification, and lemma extraction. The service runs as a multi-tenant cloud deployment with per-request isolation and concurrent support for multiple Lean 4 and Mathlib versions, accessible via a Python SDK, command-line interface, web UI, MCP server, and raw HTTP API. AXLE is publicly available and free to use at https://axle.axiommath.ai and via the axiom-axle PyPI package, with no local Lean 4 installation required. It has served over 500 million requests to date and is the underlying infrastructure for Axiom Math's proving efforts, including its 12/12 score on the 2025 Putnam competition.
Abstract（参考訳）: 我々は、Lean 4の証明操作、抽出、検証を行うクラウドサービスであるAXLE(Axiom Lean Engine)を紹介します。数学のためのAI - 強化学習パイプライン、エージェント証明ワークフロー、データセットキュレーション -- の最近の進歩は、正確で堅牢なまま数百万のリクエストにスケールするリーン4ツールを要求する。 AXLEは14のリーン4メタプログラミングツールを提供し、厳密な証明検証、宣言メタデータ抽出、セマンティックソース操作、決定論的証明の修正と単純化、レムマ抽出を提供している。サービスはマルチテナントクラウドデプロイメントとして動作し、要求毎に分離され、複数のLean 4とMathlibバージョンが同時サポートされ、Python SDK、コマンドラインインターフェース、Web UI、MPPサーバ、生のHTTP APIを介してアクセス可能である。 AXLEはhttps://axle.axiommath.aiとAxiom-axle PyPIパッケージを通じて公開されており、ローカルのLean 4インストールは不要である。これまでに5億以上のリクエストを処理し、2025年のパットナム大会の12/12スコアを含む、Axiom Mathの証明活動の基盤となる基盤となっている。

関連論文リスト

AISE-Bench: A Full-Cycle Curated Benchmark for Information Seeking on Academic Knowledge Graphs [55.8213573429699]
AISE-Benchは、学術知識グラフに基づく情報検索のための実世界のフルサイクルアノテートベンチマークである。 AISE-Benchリリースには1,133のQAペアが含まれている。クエリ、完全なAPI実行、検証されたパラメータ、リファレンスリンクによるソースグラウンドの回答などだ。我々は,回答の品質,参照基盤,API計画の正確性,実行成功を総合的に評価するプロトコルを開発した。
論文参考訳（メタデータ） (2026-06-16T07:59:46Z)
Diagnosing Knowledge Gaps in LLM Tool Use: An Agentic Benchmark for Novel API Acquisition [2.392878902712915]
NovelAPIBenchは、任意のベースモデルとターゲットライブラリの動的ベンチマークである。探索によって注入された知識とパラメトリック適応によって内部化された知識を比較した。 Retrievalは揮発性のAPIコンテンツを提供し、チューニングは手続き統合を改善する。
論文参考訳（メタデータ） (2026-06-02T13:46:04Z)
Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 [1.2816802110958607]
これは、一度精巧な証明状態をキャプチャし、Lean 4言語サーバーへの小さな拡張を通じてブランチ間で再利用します。 48のミニF2F-v2問題に対して,本手法は標準的なフォールバックよりも5.6～50倍の高速化を実現する。
論文参考訳（メタデータ） (2026-05-25T08:12:26Z)
Firefly: Illuminating Large-Scale Verified Tool-Call Data Generation from Real APIs [46.60041435990374]
本稿では,実世界のMPPサーバから検証済みのツールコールデータを生成するためのパイプラインFireFlyを紹介する。実世界のツール空間のスケールを扱うために、ペアワイズツールグラフとサンプルサブDAGを構築します。このパイプラインを適用すると、240のサーバと93のツールにまたがる5,144の検証タスクが生成される。
論文参考訳（メタデータ） (2026-05-17T17:38:17Z)
ORBIT: Scalable and Verifiable Data Generation for Search Agents on a Tight Budget [56.6320292944541]
ORBITは20Kの推論集約クエリと短い検証可能な回答を備えたトレーニングデータセットである。私たちのフレームワーク、コード、データセットはオープンソースで公開されています。
論文参考訳（メタデータ） (2026-04-01T17:42:41Z)
VerlTool: Towards Holistic Agentic Reinforcement Learning with Tool Use [78.29315418819074]
VerlToolは、体系的な設計原則を通じて制限に対処する統一的でモジュール化されたフレームワークです。我々のフレームワークはARLTをマルチターントラジェクトリとして定式化し、マルチモード観測トークン(テキスト/画像/ビデオ)を単一ターンRLVRパラダイムを超えて拡張する。モジュール化されたプラグインアーキテクチャは、軽量Python定義のみを必要とする迅速なツール統合を可能にする。
論文参考訳（メタデータ） (2025-09-01T01:45:18Z)
Not All Documents Are What You Need for Extracting Instruction Tuning Data [35.52312217796995]
本研究では,多種多様な知識を含む Web コーパスから指導用チューニングデータを抽出する手法を提案する。単純な解決策は、ドメイン固有のドキュメントを取得して、それらからすべてのQAペアを抽出することだが、これは2つの重要な課題に直面している。 EQUALは、文書の選択と高品質なQAペア抽出を交互に行う、効率的でスケーラブルなデータ抽出フレームワークである。
論文参考訳（メタデータ） (2025-05-18T06:10:08Z)
TAT-LLM: A Specialized Language Model for Discrete Reasoning over Tabular and Textual Data [73.29220562541204]
我々は,言語モデル(LLM)の驚くべきパワーを活用して課題を解決することを検討する。 LLaMA2を微調整し,既存のエキスパートアノテートデータセットから自動生成したトレーニングデータを用いてTAT-LLM言語モデルを開発する。
論文参考訳（メタデータ） (2024-01-24T04:28:50Z)
CRAFT: Customizing LLMs by Creating and Retrieving from Specialized Toolsets [75.64181719386497]
大規模言語モデル(LLM)のためのツール作成・検索フレームワークであるCRAFTを提案する。タスク用に特別にキュレートされたツールセットを作成し、複雑なタスクを解決する能力を高めるためにこれらのセットからツールを取得するコンポーネントをLLMに装備する。本手法はフレキシブルに設計されており,既製のLCMを細かな調整なしに未確認領域やモダリティに適応するためのプラグアンドプレイ方式を提供する。
論文参考訳（メタデータ） (2023-09-29T17:40:26Z)
SOLIS -- The MLOps journey from data acquisition to actionable insights [62.997667081978825]
本稿では,基本的なクロスプラットフォームテンソルフレームワークとスクリプト言語エンジンを使用しながら,すべての要件をサポートする統合デプロイメントパイプラインとフリー・ツー・オペレートアプローチを提案する。しかし、このアプローチは、実際のプロダクショングレードシステムに機械学習機能を実際にデプロイするために必要な手順やパイプラインを提供していない。
論文参考訳（メタデータ） (2021-12-22T14:45:37Z)

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

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