論文の概要: PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
- arxiv url: http://arxiv.org/abs/2610.31810v2
- Date: Mon, 26 Oct 2026 22:29:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-29 04:15:49.157862
- Title: PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
- Title（参考訳）: PaperFormalizer: リーンにおける研究論文の自動書式化の著者
- Abstract要約: リーンベースのエージェントパイプラインであるPaperFormalizerを紹介します。
PaperFormalizerは、論文をステートメントの依存性グラフに書き起こし、それぞれのステートメントを自然言語で監査し、忠実さと正確性を示し、それから形式化し、Mathlibに対するLeanのステートメントを証明します。
著者のツールキットは、より多くの論文が形式化されるにつれて成長し、著者は検証済みの論文を共有して、それに基づいて構築した研究者がリーンコードを再利用できるようにします。
- 参考スコア（独自算出の注目度）: 15.746735699356714
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.
- Abstract（参考訳）: 注意深く証明された論文でさえ、その証明や記述された仮定に小さなギャップを残すことができる。
私たちはPaperFormalizerを紹介します。これはリーンベースのエージェントパイプラインで、著者が自身の論文にそのようなギャップを見つけ、閉じ、各論文をリーン検証バージョンに変換するのに役立ちます。
LaTeXソースからPaperFormalizerは、論文をステートメントの依存性グラフに書き起こし、それぞれのステートメントを自然言語で監査し、忠実さ、あいまいさ、正確さを示し、それからLeanにおけるステートメントを公式化し、Mathlib、オプションのドメインライブラリ、著者の個人的なツールキットに対して証明する。
著者だけが、ステートメントが何を意味するのか、そして結果の形式化のギャップがいかに最も良く固定されているかを知っている。
それゆえパイプラインは停止し、著者に、声明が複数の読解を認め、自然言語とTeX記号で全ての修復を提示するたびに、著者は、著者が論文が主張するものを変える可能性のあるあらゆる決定を、著者に任せることができるという提案として、著者に尋ねる。
アウトプットは注釈付きの改訂版であり、変更の報告であり、各宣言が形式化されたステートメントにリンクされるリーンコードである。
著者のツールキットは、より多くの論文が形式化されるにつれて成長し、著者は検証済みの論文を共有して、それに基づいて構築した研究者がリーンコードを再利用できるようにします。
PaperFormalizerは、検証済みの論文を実用的に作ることによって、数学的証明に頼った研究をより堅牢にすることを目指している。
PaperFormalizerはコーディングエージェント(Claude CodeまたはCodex)内で動作し、https://github.com/Jiyuan-Tan/PaperFormalizerで利用できる。
ユーザによって共有されるリーンコードによるペーパーはhttps://paperformalizer.org.comで公開されている。
関連論文リスト
- Unfolding Scientific Papers into Multi-Turn Generation Trajectories for Continued Pre-Training [45.97752484594236]
本稿では,各紙を多ターン生成軌道に展開するパイプラインを提案する。
すべてのセクションテキストと要約は、ソースペーパーから冗長に保持される。
実際の論文テキストを回答として扱うと、SFTデータセットが生成される。
論文 参考訳（メタデータ） (2026-08-26T14:06:29Z) - Coding-agents can replicate scientific machine learning papers [0.0]
論文複製により、選択された各論文は、記録された証拠を持つターゲットを主張し、コーディングエージェントスキルとして実装する。
このワークフローにより、エージェントはこれらのターゲットを記録し、論文の手法を再構築し、計算実験を行い、生成された出力を証明とリンクさせ、論文の主張と比較する。
本論文は,4つの理科の機械学習論文における12の独立した実行について,ペーパーレプリケーションを評価した。
論文 参考訳（メタデータ） (2026-07-02T13:11:30Z) - PaperClaw: Harnessing Agents for Autonomous Research and Human-in-the-Loop Refinement [22.280674906144622]
PAPERCLAWは、研究分野から完成した論文まで、プロジェクトを自律的に行うマルチエージェントシステムである。
フルライフサイクルメモリは、各ステージを単一のリビングレコードに保持するので、長い実行は、コンテキストを失うことなく停止、検査、再開することができる。
論文 参考訳（メタデータ） (2026-06-21T17:37:01Z) - sciwrite-lint: Verification Infrastructure for the Age of Science Vibe-Writing [0.0]
現在、科学は品質保証に2つの選択肢を提供しているが、どちらも不十分である。
論文自体を測る第3の選択肢を提案する。
sciwrite-lintは、研究者のマシンで完全に動作する科学写本のためのオープンソースライブラリである。
arXivとbioRxivの未確認論文30件について, 誤り注入とLCM適応偽陽性解析を用いてパイプラインの評価を行った。
論文 参考訳（メタデータ） (2026-04-09T17:46:44Z) - FactReview: Evidence-Grounded Reviews with Literature Positioning and Execution-Based Claim Verification [57.196748998757954]
本稿では,クレーム抽出,文献位置決定,実行に基づくクレーム検証を組み合わせたエビデンスベースレビューシステムであるFactReviewを紹介する。
FactReviewは論文を提出すると、主要なクレームを特定し、その結果を報告し、論文の技術的な位置を明らかにするために近くの作業を取り出し、コードが利用可能であれば、リリースされたリポジトリを実行する。
その後、簡潔なレビューと、主要な請求を5つのラベルのうち1つに割り当てるエビデンスレポートを生成する。
論文 参考訳（メタデータ） (2026-04-05T11:45:22Z) - M2F: Automated Formalization of Mathematical Literature at Scale [24.360952996585045]
M2F(Math-to-Formal)は、リーンにおけるエンドツーエンドのプロジェクトスケールの自動形式化のための最初のエージェントフレームワークです。
約3週間で、M2Fは479ページの教科書から153,853行のリーンライブラリに変換する。
これは、通常数ヶ月または数年の専門的な努力を必要とするペースで教科書スケールの形式化を表す。
論文 参考訳（メタデータ） (2026-02-19T02:25:23Z) - Cite Pretrain: Retrieval-Free Knowledge Attribution for Large Language Models [44.31597857713689]
最初の段階でActive Indexingを導入し、一般化可能なソースアンコールバインディングを作成します。
Qwen-2.5-7B&3Bの実験は、アクティブインデックスがパッシブインデックスのベースラインを一貫して上回っていることを示している。
内部の引用は、モデルを検索ノイズに対してより堅牢にすることで、外部の引用を補完する。
論文 参考訳（メタデータ） (2025-06-21T04:48:05Z) - CausalCite: A Causal Formulation of Paper Citations [80.82622421055734]
CausalCiteは紙の意義を測定するための新しい方法だ。
これは、従来のマッチングフレームワークを高次元のテキスト埋め込みに適応させる、新しい因果推論手法であるTextMatchに基づいている。
科学専門家が報告した紙衝撃と高い相関性など,各種基準におけるCausalCiteの有効性を実証する。
論文 参考訳（メタデータ） (2023-11-05T23:09:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。