論文の概要: Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation
- arxiv url: http://arxiv.org/abs/2611.06962v1
- Date: Wed, 04 Nov 2026 08:30:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-06 21:50:50.415939
- Title: Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation
- Title（参考訳）: AI時代の逆問題の形式化:可能性、落とし穴、招待状
- Abstract要約: 古典的線形正則化理論とそれに基づく機能解析がAIエージェントによって自動形式化されているリーンライブラリであるAutoIPについて述べる。
マシンチェックされた証明は、それが証明した形式的ステートメントのみを認証するので、残りのヒューマンタスクは、それぞれの形式的ステートメントが意図されたことを確認することである。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Proof assistants such as Lean check mathematical proofs down to the axioms, and AI agents have recently made writing such proofs cheap. We describe AutoIP, a Lean library in which classical linear regularization theory, together with the functional analysis it rests on, has been autoformalized by AI agents. A machine-checked proof certifies only the formal statement it proves, so the remaining human task is to confirm that each formal statement says what was intended. We organize the library around this task: a reviewer compares the formal statements with their natural-language counterparts and never needs to read a proof. Our experience is that the risks lie in the statements rather than in the proofs, and that simple automated tests on the statements can expose problems even in the established literature. We illustrate this with a textbook theorem whose hypothesis is more restrictive than asserted. We invite the inverse problems community to extend and build on the library.
- Abstract（参考訳）: Leanのような証明アシスタントは、数学的証明を公理までチェックし、AIエージェントは最近、そのような証明を安価に書けるようにした。
古典的線形正則化理論とそれに基づく機能解析がAIエージェントによって自動形式化されているリーンライブラリであるAutoIPについて述べる。
マシンチェックされた証明は、それが証明した形式的ステートメントのみを認証するので、残りのヒューマンタスクは、それぞれの形式的ステートメントが意図されたことを確認することである。
このタスクに関するライブラリを整理する。レビュアーは、形式文と自然言語文を比較して、証明を読む必要がない。
私たちの経験では、リスクは証明にではなくステートメントの中にあり、ステートメントの単純な自動テストは、確立された文献でも問題を明らかにすることができる。
これを、仮説が主張されるよりも制限的であるような教科書の定理で説明する。
ライブラリを拡張して構築するために、逆問題コミュニティを招待します。
関連論文リスト
- Long-horizon autoformalization of a core theorem underlying MIP* = RE [2.596570510945053]
本稿では,人間の監督下でAI証明エージェントを協調するシステムであるFormalFlowを紹介する。
共有ブループリントを使用して、ネストした計画、証明、レビューループをガイドする。
我々は,古典的低次検定の量子音響性の,マシンチェックによるLean 4証明を完成させた。
論文 参考訳（メタデータ） (2026-09-17T07:26:49Z) - Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs [16.584143060150165]
我々は,5つの条件を満たす形式的なリーン証明を生成する,エージェント的・オラクル誘導型証明探索であるPristisを紹介した。
その中核は、新しい忠実に保存される分割とコンカレント検索であり、これは orderDecompose という名前で呼ばれる。
ピスティスをユークリッドの要素の最初の3冊の本に適用し、忠実な形式的証明を含む高品質なアーティファクトを創出する。
論文 参考訳（メタデータ） (2026-08-15T22:20:08Z) - Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。
最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。
汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
論文 参考訳（メタデータ） (2026-06-30T05:05:03Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。