論文の概要: Beyond Correctness: Toward Automated Novelty Verification with Lean 4
- arxiv url: http://arxiv.org/abs/2608.14669v1
- Date: Sun, 02 Aug 2026 18:49:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-23 14:54:39.955573
- Title: Beyond Correctness: Toward Automated Novelty Verification with Lean 4
- Title（参考訳）: 正確性を超えて - リーン4による自動ノベルティ検証を目指して
- Abstract要約: この記事では、記事を受け取り、Lean 4でステートメントを形式化し、3次元の意思決定ツリーを通じて、斬新な検証を発行するパイプラインを提示します。
arXivから重複が宣言されたため削除された論文の評価は、どのパフォーマンス指標よりも有益な結果となった。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Artificial intelligence systems applied to mathematics verify correctness but not novelty: an automatically generated theorem can compile in Lean without errors and yet be an already known result. This article presents AViD Journal, a pipeline that receives a LaTeX article, formalizes its statements in Lean 4, and issues a novelty verdict through a decision tree over three dimensions: prior existence in a formal corpus (Mathlib) and an informal one (TheoremSearch and Matlas, with temporal filter and LLM judge), non-triviality via automatic tactics, and structural distance between proofs measured as Jaccard distance over premise sets. Evaluation on papers withdrawn from arXiv due to declared duplication produced a result more informative than any performance measure: the identification of three obstacles that limit the approach regardless of this implementation. First, successful compilation of a Lean file does not guarantee semantic fidelity. Second, the recall ceiling is imposed by the coverage of theorem indices, not by the similarity metric. Third, arXiv removes the source code of articles upon withdrawal, compromising the reproducibility of any benchmark built upon them.
- Abstract（参考訳）: 数学に適用された人工知能システムは、正確さは検証するが、新規性ではない: 自動生成された定理は、エラーなしにリーンでコンパイルでき、既に知られている結果である。
この記事では、LaTeXの記事を受け取り、Lean 4で声明を形式化し、公式なコーパス(Mathlib)と非公式なコーパス(TheoremSearchとMatlas、時間的フィルターとLCMの判断を含む)、自動戦術による非自明性、前提セット上のジャカード距離として測定された証明の間の構造的距離という、3つの次元にわたる決定ツリーを通じて、斬新な検証を発行するパイプラインであるAViD Journalを紹介します。
arXivから重複が宣言されたために削除された論文の評価は、どのパフォーマンス指標よりも有益な結果を生み出した。
第一に、Leanファイルの正常なコンパイルはセマンティックな忠実さを保証しません。
第二に、リコール天井は、類似度メートル法ではなく、定理指標のカバレッジによって課される。
第3に、arXivは、削除時に記事のソースコードを削除し、それら上に構築されたベンチマークの再現性を損なう。
関連論文リスト
- AI-Assisted Discovery and Construction of a Counterexample to the Convergence of Three-Block ADMM with the Identity Matrix as its Third Constraint Block [7.333795130390353]
直接3ブロックADMMは,最初の2ブロックが強い凸二次群である場合でも収束しない可能性があることを示す。
また,乗算緩和の研究を指導し,定位・クラスレベルで収束を回復できるかを明らかにする。
論文 参考訳（メタデータ） (2026-08-14T15:36:32Z) - MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
我々は、数学者がAIシステムに指示することで、Lean 4証明アシスタントの研究結果を形式化し、そのアクティビティを形式化ゲームとしてフレーム化する。
目的は文書をリーンに変えることである。ゲームは開発がコンパイルされたときに勝利し、残念なことは含まない。マシンチェックは、目標定理がリーンの基本公理にのみ依存していることを示している。
ケーススタディは、ドブルシンの平均場経路を通した非線形ブラソフ方程式の正当性に対する完全で公理クリーンな定式化である。
論文 参考訳（メタデータ） (2026-07-09T23:17:54Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - Convergence Theory for Iterative LLM-Based Neural Architecture Search: A Parametric Cross-Entropy Framework with Closed-Form Proxy Reliability [48.83701310501069]
大規模言語モデル(LLM)は、反復型ニューラルアーキテクチャサーチ(NAS)におけるジェネレータとしてますます使われている。
我々は,LCM-NASを,実行可能プログラム上でのパラメトリッククロスエントロピー(CE)法としてモデル化する。
我々は,(1)エリートアーキテクチャの反復LEM微調整は,LLMファミリーに制限されたCE更新と同等であり,(2)期待されるアーキテクチャ品質はサイクル毎に単調に低下せず,(3)エリートセットの確率は幾何率で一定点に収束する,という6つの結果を示した。
論文 参考訳（メタデータ） (2026-05-28T15:45:19Z) - Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof [0.0]
LLM駆動のランタイムによってどのようにスキルが消費されるかに忠実なスキル行動に関する正確なセマンティクスを提供します。
本稿では,定式化や定式化によるスキル向上を両立させる構成可能な3つの手法を提案する。
これら3つのメソッドに加えて、バンドルプロデューサと再チェッカーは、オープンソースエンクロードフレームワークのゼロ依存JavaScriptモジュールとして出荷される。
論文 参考訳（メタデータ） (2026-05-09T19:27:38Z) - Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game [0.0]
本稿では,将来の自動定理発見AIに必要な機能としてアーキテクチャ推論を取り上げる。
リーン4のNatural Number Gameで識別子をリネームすることで、ゼロ知識でクローズドな環境を作りました。
我々は最先端のモデルを評価し、難読化が推論時間を増加させる普遍的な遅延税を求める。
論文 参考訳（メタデータ） (2026-05-01T14:03:05Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - What Papers Don't Tell You: Recovering Tacit Knowledge for Automated Paper Reproduction [57.86097956633207]
Methodは、学術論文から実行可能なコードを生成するグラフベースのエージェントフレームワークである。
3つのドメイン、10のタスク、10の最近の論文にまたがる拡張ReproduceBenchでは、公式実装に対する平均的なパフォーマンスギャップが10.04%に達する。
論文 参考訳（メタデータ） (2026-03-02T12:33:31Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳（メタデータ） (2023-10-23T17:58:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。