論文の概要: LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

• arxiv url: http://arxiv.org/abs/2607.20503v1
• Date: Fri, 26 Jun 2026 15:43:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-27 00:46:13.205688
• Title: LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
• Title（参考訳）: LeanFlow: ワークフロー駆動型リーン自動化のケーススタディ
• Abstract要約: 数理論文を構築可能なリーンプロジェクトに翻訳するためのLLMエージェントシステムであるLeanFlowを提示し、評価する。 近年のバリデーション・イン・ザ・ループシステムでは,大規模な形式的アーティファクトを生成可能であるが,どの実行機構が文書からプロジェクトへの形式化の完了,監査性,効率に影響を及ぼすかは定かではない。 本研究では,数論と測度論の未定な2つの数学的論文のケーススタディを通じて,Kimi2.6 と GPT5.5 を用いたモデル,証明-ワークフロー,アブレーションについて検討する。
• 参考スコア（独自算出の注目度）: 3.08055258820978
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: We present and evaluate LeanFlow, an LLM agent system specialized for translating mathematical papers into buildable Lean projects. Recent verifier-in-the-loop systems show that large formal artifacts can be produced, but it remains unclear which runtime mechanisms affect completion, auditability, or efficiency in document-to-project formalization. We study this question through case studies on two previously unformalized mathematical papers in number theory and measure theory, using model, proof-workflow, and toolset ablations with Kimi2.6 and GPT5.5; we report task outcome, API calls, input tokens, and output tokens. With Kimi2.6, the full workflow completes both document-level projects within the 2000-call budget, while no-queue variants reach the budget limit; with GPT5.5, all document-level variants complete, and the full workflow has the lowest or tied-lowest input-token cost on both sources. As complementary calibration, LeanFlow reaches 75.7% BEq+ on the PFR slice of RLM25 and solves all five ICML 2026 AI for Math TCS challenge projects in our GPT5.5 runs.
• Abstract（参考訳）: 数理論文を構築可能なリーンプロジェクトに翻訳するためのLLMエージェントシステムであるLeanFlowを提示し、評価する。 近年のバリデーション・イン・ザ・ループシステムでは,大規模な形式的アーティファクトを生成可能であるが,どの実行機構が文書からプロジェクトへの形式化の完了,監査性,効率に影響を及ぼすかは定かではない。 本研究では,Kimi2.6 と GPT5.5 を用いて,数論と測度論の未定な2つの数学的論文をケーススタディとして検討し,タスク結果,API コール,入力トークン,出力トークンについて報告する。 Kimi2.6では、完全なワークフローが2000呼び出し予算内でドキュメントレベルのプロジェクトの両方を完了し、非キューのバリエーションが予算の限界に達し、GPT5.5ではすべてのドキュメントレベルのバージョンが完了し、フルワークフローは、両方のソースで最低または最も低いインプット・ツーケン・コストを持つ。 補完的なキャリブレーションとして、LeanFlowはRLM25のPFRスライスで75.7%のBEq+に達し、GPT5.5実行中の5つのICML 2026 AI for Math TCS課題プロジェクトを解決します。

関連論文リスト

• RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflows [8.700422995850152]
  State-of-the-art (SOTA) LLMは、証明ベースのOlympiad問題から、IMO 2025問題のほとんどを解決するまで、進歩してきた。 本稿では,90 Gemini 2.5 Pro生成ソリューションのコーパスを用いて,詳細なエラーアノテーションを用いた1-4スケールで評価を行った。 分析の結果、モデルが不正確な解を確実にフラグ付けできるが、部分クレジットの割り当て方法にキャリブレーションのギャップがあることがわかった。
  論文  参考訳（メタデータ） (2025-10-10T05:47:40Z)
• WorkflowLLM: Enhancing Workflow Orchestration Capability of Large Language Models [105.46456444315693]
  ワークフローオーケストレーションにおける大規模言語モデルの能力を高めるための,データ中心のフレームワークであるLLMを提案する。 最初は106,763のサンプルで大規模な微調整Benchを構築し、28のカテゴリにわたる83のアプリケーションから1,503のAPIをカバーしている。 LlamaLlamaは複雑なAPIをオーケストレーションする能力を示しながら、優れた一般化性能を実現している。
  論文  参考訳（メタデータ） (2024-11-08T09:58:02Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• AFlow: Automating Agentic Workflow Generation [36.61172223528231]
  大規模言語モデル(LLM)は、様々な領域にわたる複雑なタスクを解く上で、顕著な可能性を示している。 我々は、Monte Carlo Tree Searchを使って、この空間を効率的に探索する自動化フレームワークであるAFlowを紹介します。 6つのベンチマークデータセットに対する実証的な評価は、AFlowの有効性を示し、最先端のベースラインよりも平均5.7%向上している。
  論文  参考訳（メタデータ） (2024-10-14T17:40:40Z)
• Benchmarking Agentic Workflow Generation [80.74757493266057]
  複数面シナリオと複雑なグラフワークフロー構造を備えた統合ワークフロー生成ベンチマークであるWorfBenchを紹介する。 また,サブシーケンスとサブグラフマッチングアルゴリズムを利用したシステム評価プロトコルWorfEvalを提案する。 我々は、生成されたタスクが下流のタスクを強化し、推論中により少ない時間で優れたパフォーマンスを達成することを観察する。
  論文  参考訳（メタデータ） (2024-10-10T12:41:19Z)
• FlowBench: Revisiting and Benchmarking Workflow-Guided Planning for LLM-based Agents [64.1759086221016]
  ワークフロー誘導計画の最初のベンチマークであるFlowBenchを紹介します。 FlowBenchは6つのドメインから51のシナリオをカバーしている。 以上の結果から,現在のLLMエージェントは良好な計画を立てるためにかなりの改善が必要であることが示唆された。
  論文  参考訳（メタデータ） (2024-06-21T06:13:00Z)

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

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