論文の概要: Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
- arxiv url: http://arxiv.org/abs/2606.14000v1
- Date: Fri, 12 Jun 2026 00:45:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-15 16:00:42.697475
- Title: Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
- Title（参考訳）: フォーマライズ・数値解析:カーネル・アクセプタンスを超えたエージェント・パイプラインと品質監査
- Authors: Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess, Vasily Ilin,
- Abstract要約: コーディングエージェントはLean 4で高度な数学教科書全体を形式化できます。
本稿では,コンパイラを超えてエージェント生成形式の品質を評価するためのフレームワークを提案する。
以上の結果から,コンパイルベースのメトリクスは形式化品質を大幅に上回っていることが示唆された。
- 参考スコア（独自算出の注目度）: 0.3624700141426058
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Recent work has demonstrated that coding agents can formalize entire advanced mathematics textbooks in Lean 4, yet existing efforts concentrate on branches of mathematics already well-represented in mathlib and measure success solely through kernel acceptance. We address both limitations by applying a coding agent to formalize Numerical Methods for Ordinary Differential Equations, a textbook in numerical analysis that is largely absent from mathlib, stressing the agent's capacity to develop new theory from scratch. We further introduce a systematic, reproducible three-dimensional framework for evaluating the quality of agent-produced formalizations beyond compilation: semantic correctness, Mathlib reuse, and cross-file reuse via LLM-as-judge methods. Applying this framework to our own formalization and to the released outputs of RepoProver and M2F, we uncover recurring unfaithful formalization patterns, including incomplete multi-part statements, added weakening hypotheses, and parameter restrictions, that kernel acceptance entirely obscures. Our results suggest that compilation-based metrics substantially overstate formalization quality, and we provide a reproducible audit methodology to support more rigorous evaluation of future autoformalization systems.
- Abstract（参考訳）: 最近の研究は、コーディングエージェントがLean 4の高度な数学教科書全体を形式化できることを示したが、既存の取り組みは数学の分野に集中しており、すでに数学でよく表現されており、カーネルの受け入れによってのみ成功を測定する。
数値解析の教科書である正規微分方程式の数値解法を定式化するために符号化エージェントを適用することにより、両者の制約に対処し、エージェントがゼロから新しい理論を開発する能力を強調した。
さらに,コンパイル以上のエージェント生成形式化の質を評価するための,体系的かつ再現可能な3次元フレームワーク,意味的正しさ,Mathlib再利用,LCM-as-judge法によるファイル間再利用を提案する。
このフレームワークを私たち自身の形式化や、RepoProverとM2Fのリリースした出力に適用することで、不完全な多部文、弱体化仮説、パラメータ制限など、カーネルの受け入れを完全に曖昧にする不誠実な形式化パターンが繰り返し発見されるのです。
以上の結果から,コンパイルベースのメトリクスは形式化品質を大幅に上回るものであることが示唆され,将来的な自動形式化システムの厳密な評価を支援する再現可能な監査手法が提供される。
関連論文リスト
- Lean-GAP: A Dataset of Formalized Graduate Algebra Problems [3.1963549333419388]
本稿では,PDF-to-La Algebra前処理,Lean 4への自動形式化,非公式な形式対応の検証などからなるスケーラブルなパイプラインを開発する。
コントリビューションには、(i)形式化された演習の構造化データセットの構築、(ii)教科書数学の形式化のための体系的方法論、(iii)形式化過程における繰り返しの課題の分析が含まれる。
論文 参考訳（メタデータ） (2026-05-20T08:15:43Z) - Reasoning over mathematical objects: on-policy reward modeling and test time aggregation [120.92237765735813]
数学的オブジェクト、Principiaスイートを導出するためのトレーニングデータとベンチマークを構築し、リリースする。
オンライントレーニングは,アグリゲーションによるテスト時間計算のスケールアップにも有効であることを示す。
Qwen3-235Bやo3のような強力なLMがプリンキピアで苦戦しているのに対して、トレーニングレシピは大幅に改善されている。
論文 参考訳（メタデータ） (2026-03-19T13:27:12Z) - MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。
さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
論文 参考訳（メタデータ） (2026-01-30T15:24:42Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。
これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。
我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
論文 参考訳（メタデータ） (2025-10-12T21:42:04Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。
このモデルは、微粒な類似性計算法と再ランクモジュールを応用した、対照的な学習フレームワークで学習される。
実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。
論文 参考訳（メタデータ） (2025-01-21T06:32:25Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。