論文の概要: KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents

• arxiv url: http://arxiv.org/abs/2610.35596v1
• Date: Mon, 26 Oct 2026 15:22:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 22:27:14.05185
• Title: KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
• Title（参考訳）: KAPPA:Lean 4とLanguage Model Agentによる統計論文の証明
• Abstract要約: 本稿では,言語モデルエージェントを編成するオープンソースソフトウェアであるKAPPA(Kit of Agents for Proof-checking Papers with a proof Assistant)を紹介する。 論文の証明をライブラリのMathlibで証明アシスタントのLean 4に変換して,その結果を確認する。 設計を記述し、完全な実行を通し、キットを回答キー付きの4つのサンプル論文と3つの統計論文に適用し、公開修正前のバージョンに盲目でチェックする。
• 参考スコア（独自算出の注目度）: 4.82972978331848
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organizes language model agents, run by Claude Code, to translate the proofs of a LaTeX paper into the proof assistant Lean 4 with its library Mathlib and check them there, result by result. Each numbered result receives one of four verdicts: verified unconditionally; verified conditionally, with every cited or unproved input stated as a named hypothesis; issue recorded, with its place in the paper and the side at fault; or unfinished, with the reason. The kit follows the paper's own proof step by step, rather than finding a new one. Separate agents write and review, each statement is compared with the paper before it is proved and fingerprinted afterwards, and every verdict rests on evidence that can be rerun without a language model. The kit runs unattended for hours, waits out usage limits, re-checks only what a revision changed and reports its cost by role, model and result. We describe the design, walk through a complete run, and apply the kit to four example papers with answer keys and to three published statistical papers, checked blind in their versions from before public corrections. In all three, the kit found the published error at the step that the correction names, together with further problems that we confirmed by hand. Given the same papers directly, the same language model working with Lean classified fewer results correctly on the longest paper and reported some statements narrower than the paper's as proved; no verdict of the kit claimed more than its Lean evidence showed.
• Abstract（参考訳）: 統計学の論文は、読者が列に並ぶことの少ない長い証明に基づいている。 我々は、Claude Codeが運営する言語モデルエージェントを組織するオープンソースソフトウェアであるKAPPA(Kit of Agents for Proof-checking Papers with a proof Assistant)を紹介し、LaTeXの論文の証明をライブラリであるMathlibで証明アシスタントLean 4に翻訳し、その結果を結果として確認する。 それぞれの数値は4つの評定のうちの1つを受け取っている: 条件付き検証; 条件付き検証; 名前付き仮説として記述された全ての引用または未証明の入力; 問題の記録; 紙と欠点の側にある; または理由により未完成である。 キットは、新しいものを見つけるのではなく、紙の証明をステップバイステップで行う。 エージェントを別々に書き、レビューし、各ステートメントは証明する前に論文と比較され、その後指紋で示され、全ての評決は言語モデルなしで再実行できる証拠に依存している。 キットは数時間無調整で動作し、使用制限を待ち、リビジョンの変更点だけを再チェックし、役割やモデル、結果によってコストを報告する。 設計を記述し、完全な実行を通し、キットを回答キー付きの4つのサンプル論文と3つの統計論文に適用し、公開修正前のバージョンに盲目でチェックする。 これら3つの中で、このキットは、修正の名前が手作業で確認したさらなる問題と共に公表されたエラーを発見した。 同じ論文を直接考えると、Leanで作業する同じ言語モデルは、最も長い論文で正しく結果を分類し、証明された論文よりも狭い声明を報告しました。

関連論文リスト

• PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean [15.74673569935671]
  リーンベースのエージェントパイプラインであるPaperFormalizerを紹介します。 PaperFormalizerは、論文をステートメントの依存性グラフに書き起こし、それぞれのステートメントを自然言語で監査し、忠実さと正確性を示し、それから形式化し、Mathlibに対するLeanのステートメントを証明します。 著者のツールキットは、より多くの論文が形式化されるにつれて成長し、著者は検証済みの論文を共有して、それに基づいて構築した研究者がリーンコードを再利用できるようにします。
  論文  参考訳（メタデータ） (2026-10-22T18:46:53Z)
• Calibrating Interpretability Instruments Before Trusting Their Verdicts [1.0829694003408499]
  Causal氏は、大きな言語モデル(LLM)の内部は測定にかかっていると主張している。 これらの測定は、エラーではなく可算数を返す特定の診断可能な方法で失敗する。 このノートは、拒絶と道徳的表現に関する因果的解釈可能性プログラムの6つの失敗を文書化している。
  論文  参考訳（メタデータ） (2026-09-13T19:37:02Z)
• Coding-agents can replicate scientific machine learning papers [0.0]
  論文複製により、選択された各論文は、記録された証拠を持つターゲットを主張し、コーディングエージェントスキルとして実装する。 このワークフローにより、エージェントはこれらのターゲットを記録し、論文の手法を再構築し、計算実験を行い、生成された出力を証明とリンクさせ、論文の主張と比較する。 本論文は,4つの理科の機械学習論文における12の独立した実行について,ペーパーレプリケーションを評価した。
  論文  参考訳（メタデータ） (2026-07-02T13:11:30Z)
• Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving [13.87786274932945]
  リーンで証明されたLCM支援定理のベンチマークは、すべての解決されたインスタンスがマシンチェックされた証明を持ってくるため、本質的に信頼できるものとして扱われることが多い。 コーパススケールの静的チェッカーを用いて4,833個の結果を得た。 本稿では,フォールト分類法,自動チェッカーとリコール指向のセマンティック監査プロンプト,および公式な数学データセットの作成を導くための標準リリースを提案する。
  論文  参考訳（メタデータ） (2026-06-28T16:46:36Z)
• FactReview: Evidence-Grounded Reviews with Literature Positioning and Execution-Based Claim Verification [57.196748998757954]
  本稿では,クレーム抽出,文献位置決定,実行に基づくクレーム検証を組み合わせたエビデンスベースレビューシステムであるFactReviewを紹介する。 FactReviewは論文を提出すると、主要なクレームを特定し、その結果を報告し、論文の技術的な位置を明らかにするために近くの作業を取り出し、コードが利用可能であれば、リリースされたリポジトリを実行する。 その後、簡潔なレビューと、主要な請求を5つのラベルのうち1つに割り当てるエビデンスレポートを生成する。
  論文  参考訳（メタデータ） (2026-04-05T11:45:22Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Evidence-based Factual Error Correction [18.52583883901634]
  本稿では,事実誤り訂正の課題を紹介する。 これは、反論されるか、証拠によって部分的にのみ支持される文章を訂正するメカニズムを提供する。
  論文  参考訳（メタデータ） (2021-06-02T11:00:17Z)

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

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