論文の概要: MerLean: An Agentic Framework for Autoformalization in Quantum Computation

• arxiv url: http://arxiv.org/abs/2602.16554v1
• Date: Wed, 18 Feb 2026 15:54:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-19 15:58:30.638258
• Title: MerLean: An Agentic Framework for Autoformalization in Quantum Computation
• Title（参考訳）: MerLean: 量子計算におけるオートフォーマル化のためのエージェントフレームワーク
• Authors: Yuanjie Ren, Jinzheng Li, Yidi Qi,
• Abstract要約: 本稿では,量子計算におけるオートフォーマル化のための完全に自動化されたフレームワークであるMerLeanを紹介する。 MerLeanはLaLeanソースファイルからステートメントを抽出し、Mathlib上に構築された検証済みのLean4コードに形式化し、結果を人間可読なLaLean宣言に変換してセマンティックレビューを行う。 我々はMerLeanを114のステートメントから2,050のリーンステートメントを生成する3つの理論量子コンピューティング論文で評価した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \LaTeX{} source files, formalizes them into verified Lean~4 code built on Mathlib, and translates the result back into human-readable \LaTeX{} for semantic review. We evaluate MerLean on three theoretical quantum computing papers producing 2,050 Lean declarations from 114 statements in total. MerLean achieves end-to-end formalization on all three papers, reducing the verification burden to only the newly introduced definitions and axioms. Our results demonstrate that agentic autoformalization can scale to frontier research, offering both a practical tool for machine-verified peer review and a scalable engine for mining high-quality synthetic data to train future reasoning models. Our approach can also be generalized to any other rigorous research in mathematics and theoretical physics.
• Abstract（参考訳）: 本稿では,量子計算におけるオートフォーマル化のための完全に自動化されたエージェントフレームワークであるMerLeanを紹介する。 MerLean は \LaTeX{} ソースファイルから数学的ステートメントを抽出し、それを Mathlib 上に構築された検証済みの Lean~4 コードに形式化し、結果をセマンティックレビューのために可読な \LaTeX{} に変換する。 我々はMerLeanを114の文から2,050のリーン宣言を生成する3つの理論量子コンピューティング論文で評価した。 MerLeanは3つの論文すべてでエンドツーエンドの形式化を実現し、検証の負担を新たに導入された定義と公理のみに減らした。 その結果,エージェントによるオートフォーマル化がフロンティア研究に拡張できることが示され,マシン検証ピアレビューのための実用的なツールと,高品質な合成データをマイニングして将来の推論モデルを訓練するためのスケーラブルなエンジンが提供される。 我々のアプローチは、数学や理論物理学における他の厳密な研究にも一般化することができる。

関連論文リスト

• Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
  本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。 エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。 この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
  論文  参考訳（メタデータ） (2026-02-02T16:24:53Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。 さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
  論文  参考訳（メタデータ） (2026-01-30T15:24:42Z)
• Quantum Many-Body Physics Calculations with Large Language Models [7.679615503214482]
  大規模言語モデル(LLM)は、複数のドメインで複雑なタスクを実行する前例のない能力を示している。 我々は、量子物理学において広く用いられている近似法、Hartree-Fock法に焦点をあてる。 解析計算を標準化されたステップに分解する多段階プロンプトテンプレートを設計する。 我々は過去10年間の15の研究論文の計算におけるGPT-4の性能を評価した。
  論文  参考訳（メタデータ） (2024-03-05T17:47:22Z)
• InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning [98.53491178426492]
  InternLM2から事前学習を継続するILMs InternLM-Mathをオープンソースとして公開する。 我々は、連鎖推論、報酬モデリング、形式推論、データ拡張、コードインタプリタを、統一されたSeq2seqフォーマットで統一する。 我々の事前学習モデルは、微調整なしでMiniF2Fテストセットで30.3を達成する。
  論文  参考訳（メタデータ） (2024-02-09T11:22:08Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)

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

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