論文の概要: ProofPatch: Reviewing Lean Statements and Keeping the Reviews Valid as Formalizations Evolve
- arxiv url: http://arxiv.org/abs/2611.01357v1
- Date: Sat, 31 Oct 2026 23:55:48 GMT
- ステータス: 情報取得中
- システム内更新日: 2026-11-03 19:19:25.649046
- Title: ProofPatch: Reviewing Lean Statements and Keeping the Reviews Valid as Formalizations Evolve
- Title（参考訳）: ProofPatch: リーンのステートメントをレビューし、レビューを形式化として有効に保つ
- Abstract要約: ProofPatchは、レビュアがリーンのステートメントを判断し、開発が変化している間に判断を有効に保つのに役立つツールです。
レビュアーは、仮説が必要かどうか、あるいは反例が存在するかどうかなど、カーネルが対象とするステートメントに関する質問をすることができる。
それぞれの決定には,文の指紋が格納されている。Lean氏はそれを詳しく説明した上で,それが依存する定義を詳しく説明した上で,それを変更するパッチがブロックされるように,宣言をピン留めすることができる。
- 参考スコア（独自算出の注目度）: 4.256509040406718
- License:
- Abstract: The kernel of the Lean proof assistant checks that a proof establishes its statement. Whether the statement says what was intended is left to human reviewers. This is the old problem of validating a specification, and it grows more pressing as language models write formal statements in bulk and agents edit formal developments continuously. We present ProofPatch, a tool that helps reviewers judge Lean statements and keeps their judgments valid while the development changes. A reviewer can ask the kernel targeted questions about a statement, such as whether a hypothesis is needed or whether a counterexample exists. Each decision is stored with fingerprints of the statement as Lean elaborated it and of the definitions it depends on, and any declaration can be pinned so that a patch changing it is blocked, whether a person or an agent built on a large language model (LLM) wrote the patch. Working on elaborated terms rather than source text is the central design choice: notation and formatting changes leave a decision intact, and a changed definition reaches every theorem that uses it. On 229 pairs of consecutive revisions of Mathlib, Lean's mathematics library, ProofPatch sends 118 of 12,898 synthetic decisions back for review. Every text-based alternative misses at least 38 of these or sends back at least 13 times as many. On 1,527 labeled statements, kernel evidence flags unfaithful ones with precision 0.88 to 0.96, and in 344 runs of an LLM agent no change to a pinned statement got through.
- Abstract（参考訳）: Leanの証明アシスタントのカーネルは、証明がそのステートメントを確立することをチェックします。
声明が何を意図したかは、人間のレビュアーに委ねられている。
これは仕様を検証する古い問題であり、言語モデルがバルクで形式的なステートメントを記述し、エージェントが形式的な開発を継続的に編集するにつれて、より圧力がかかります。
ProofPatchは、レビュアがリーンのステートメントを判断し、開発が変化している間に判断を有効に保つのに役立つツールです。
レビュアーは、仮説が必要かどうか、あるいは反例が存在するかどうかなど、カーネルが対象とするステートメントに関する質問をすることができる。
それぞれの決定には、文の指紋と、それが依存する定義が格納され、大きな言語モデル(LLM)上に構築された人やエージェントがパッチを書いたかどうかに関わらず、変更するパッチがブロックされるように、宣言をピン留めすることができる。
表記と書式の変更は決定をそのまま残し、変更の定義はそれを使用するすべての定理に達する。
リーンの数学ライブラリであるMathlibの229の連続的な改訂で、ProofPatchは12,898の合成決定を118通送ってレビューしている。
テキストベースの代替手段は、少なくとも38個を逃すか、少なくとも13倍の数を返送する。
1,527のラベル付き文では、カーネルのエビデンスフラグが0.88から0.96の精度で不信なものとなり、LCMエージェントの44回の動作では、ピン付きステートメントの変更は行われなかった。
関連論文リスト
- OneCodeReviewBench: Typed Decisions for Code Review and Search [0.0]
12のプログラミング言語とYAMLにまたがる1,968の合成ケースであるOneCodeReviewBenchを紹介します。
明示的なコントラクトはランタイムの仮定、ソーススコープ、回答基準を指定する。
論文 参考訳（メタデータ） (2026-10-24T01:40:29Z) - SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner [0.0]
SCOPE(State-Conditioned Operator Planning and Execution)は、労働の自然な分割を強制する。
システムはオペレータの語彙を計画し、シンボルエンジンが数値を実行し、コンパイラが証明をレンダリングする。
システム認証は191/218 (87.6%) で、バックボーンは135Mである。
論文 参考訳（メタデータ） (2026-10-06T13:22:24Z) - IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。
提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。
IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
論文 参考訳（メタデータ） (2026-09-09T17:59:04Z) - VeriPhy: Agentic Physical Reasoning for World Model Evaluation and Refinement [57.86962208273888]
テキストのみのプランナが入力された物理義務にプロンプトをコンパイルする監査可能な物理検証システムを提案する。
それぞれのアクションは、ペイロードがタイプされた測定か、明示的にタグ付けされた学習状態である証明付きエビデンスレコードを返す。
我々は, 実発生障害を即時参照, 空間, 時間でローカライズする, 1500クリックの欠陥記録のコーパスにおいて, 評価をアンロックする。
論文 参考訳（メタデータ） (2026-09-02T20:36:45Z) - Measuring the Checker: Mutation Analysis for GPU-Kernel Benchmark Oracles [86.41218924166775]
LLM生成のGPUカーネルのベンチマークは、ランダムな入力とゆるやかな浮動小数点耐性で正確性を決定する。
最近の研究は、これらのチェッカーは弱く、手動でパッチを当てることに同意している。
本稿では,カーネルベンチマークの精度指標として突然変異解析を導入する。
論文 参考訳（メタデータ） (2026-09-02T10:30:05Z) - PatchWrite: One Line, Not One Section -- Compile-Gated, Validity-Preserving Editing for AI-Drafted Manuscripts [2.7819582252059405]
PatchWriteは、候補編集がコミットされた原稿状態になる方法を制約する。
EDIT N Mの編集とロールバックを再利用するが、コンパイルの受け入れを致命的なログチェックで制限する。
いずれのチェックも失敗する候補は拒否され、前のHEADは保持される。
論文 参考訳（メタデータ） (2026-08-24T09:04:19Z) - Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。
ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
論文 参考訳（メタデータ） (2026-06-30T00:27:53Z) - FactReview: Evidence-Grounded Reviews with Literature Positioning and Execution-Based Claim Verification [57.196748998757954]
本稿では,クレーム抽出,文献位置決定,実行に基づくクレーム検証を組み合わせたエビデンスベースレビューシステムであるFactReviewを紹介する。
FactReviewは論文を提出すると、主要なクレームを特定し、その結果を報告し、論文の技術的な位置を明らかにするために近くの作業を取り出し、コードが利用可能であれば、リリースされたリポジトリを実行する。
その後、簡潔なレビューと、主要な請求を5つのラベルのうち1つに割り当てるエビデンスレポートを生成する。
論文 参考訳（メタデータ） (2026-04-05T11:45:22Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。