論文の概要: PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs
- arxiv url: http://arxiv.org/abs/2607.16997v1
- Date: Sat, 18 Jul 2026 23:10:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-21 18:48:37.333662
- Title: PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs
- Title（参考訳）: PriorProof:フォーマルな証明のためのテクニックノベルティのポイント・イン・タイム測定
- Abstract要約: 我々は、形式数学における時間相対的証明-ルート非標準性という、意図的なより狭い構成について研究する。
PriorProofは、その精巧な証明項の依存関係のフットプリントを抽出し、そのフットプリントの重み付けされた推定値をスコアする。
我々は、スコアギャップが解釈可能な信頼性指標を提供する分解可能な時間アンコール信号として、PreferProofを提案する。
- 参考スコア（独自算出の注目度）: 0.23689955632456092
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Mathematicians distinguish proofs that explain, simplify, or introduce a nonstandard route, but these judgments are difficult to operationalize. We study a deliberately narrower construct: time-relative proof-route nonstandardness in formal mathematics. For a Lean theorem, PriorProof extracts the dependency footprint of its elaborated proof term and scores the weighted surprisal of that footprint under a retrieval-conditioned, hierarchically smoothed prior built only from an earlier quarterly snapshot of Mathlib. The method requires no hand-built technique ontology and no human labels: statement retrieval is learned from proof-derived contrastive pairs, while the scored object is read mechanically from proof terms. In a blinded topology study, 100 presentations collapse to 76 distinct underlying pairs: 12 canonical contrasts shown three times for consistency screening and 64 distinct stratified pairs. Against the majority of three retained domain raters, PriorProof agrees on 53/76 pairs (69.7%, Wilson 95% CI 58.7-78.9%), including 11/12 canonical pairs (91.7%, 64.6-98.5%) and 42/64 stratified pairs (65.6%, 53.4-76.1%). Score-gap quartiles are nonmonotone after repeat collapse; the endpoints are 12/19 (63.2%, 41.0-80.9%) in the smallest-gap bin and 16/19 (84.2%, 62.4-94.5%) in the largest, supporting an endpoint-calibration tendency rather than a resolved staircase. The best language-model condition agrees on 60/76 pairs (78.9%, 68.5-86.6%); on paired outcomes, PriorProof alone is correct on 8 pairs and the model alone on 15 (exact two-sided McNemar p = 0.210), so the difference is not established at this sample size. We therefore present PriorProof not as a replacement for expert or model judgment, but as a decomposable, time-anchored signal whose score gap provides an interpretable reliability indicator.
- Abstract（参考訳）: 数学者は非標準経路の説明、単純化、導入の証明を区別するが、これらの判断は運用が難しい。
我々は、形式数学における時間相対的証明-ルート非標準性という、意図的に狭められた構成について研究する。
リーンの定理では、PreferProofはその精巧な証明項の依存関係のフットプリントを抽出し、そのフットプリントの重み付けされた仮定を検索条件付き階層的にスムーズなMathlibの以前の四半期スナップショットからのみ作成する。
この方法は手作りの技法オントロジーを必要とせず、人間のラベルも必要としない: 文検索は証明から派生したコントラッシブなペアから学習され、得られたオブジェクトは証明項から機械的に読み取られる。
ブラインドトポロジ研究では、100のプレゼンテーションが76の異なるペアに崩壊し、12の標準コントラストが3回、64の異なる階層化されたペアが3回表示された。
3つのドメインラベスターの大半に対して、PresideProofは53/76対(69.7%、Wilson 95% CI 58.7-78.9%)、11/12標準対(91.7%、64.6-98.5%)、42/64成層対(65.6%、53.4-76.1%)で合意している。
スコアギャップ四重項は、繰り返し崩壊した後に非単調で、最小のギャップビンでは12/19(63.2%、41.0-80.9%)、最大では16/19(84.2%、62.4-94.5%)であり、解決された階段よりもエンドポイントの校正傾向を支持する。
最高の言語モデル条件は、60/76対(78.9%、68.5-86.6%)で一致し、ペアの結果では、PresideProof単独は8対、モデル単独は15対(正確にはMcNemar p = 0.210)である。
そこで本稿では,PriorProofを専門家やモデル判断の代替としてではなく,スコアギャップが解釈可能な信頼性指標を提供する分解可能な時間アンコール信号として提示する。
関連論文リスト
- Marginal Fidelity Does Not Establish User Simulation in Demographic Synthetic Survey Panels: Response Contracts, Support Collapse and Conditioning Failure [51.736723807086385]
人口密着協定は、個別のシミュレーションの証拠ではなく、エスカレーション契約の証拠であり、シミュレーションされた回答者なしで得られる推定値である。
9つのアライメントされたモデルバッテリペアでは、非個人個体数のクエリの平均は6.27 MAE対12.39であり、9つの比較すべてで勝利する。
論文 参考訳（メタデータ） (2026-09-07T10:22:22Z) - Reliable Benchmarking of Artifact Detection in Computational Pathology: A Reproducibility and Uncertainty Analysis [1.8864137667201766]
メソッド: このプロトコルは、テストセットサンプリング、トレーニング性、パーティション構成、文書化前処理の4つの変数ソースを定量化する。
拡散型人工物検出装置を独立に再構築し, 元の24スライディング分割と教師付きベースラインに対して評価した。
結果: 本手法の中枢機構は、補助的コントラスト項は、プールされたF1を0.673から0.688に改善し、第2シードで複製する。
論文 参考訳（メタデータ） (2026-08-31T14:07:15Z) - Agreement Before Diversity: Verification-First Complementarity for Heterogeneous Language-Model Coordination [11.215813718564283]
候補のヘッドルームを置換権限から切り離し、後者を明示的で監査可能なオブジェクトとします。
提案手法であるCon Agreement-Before-Diversityは,フリーフリーでラベルのない決定ルールである。
論文 参考訳（メタデータ） (2026-08-05T09:24:39Z) - Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
PointArena 2026は77.2%の精度でベンチマークで2位である。
ap proachは3つの障害モードをターゲットにしている。第一に、エージェント駆動のシンセシスは大きなセマンティクスとアンカー相対的な候補プールを構築する。
次に、determinis tic steerable-dataパイプラインは、認証された10,000サンプルのメインセットと、マスク、テンプレート、パス検証を使用するリザーブサンプルを生成する。
論文 参考訳（メタデータ） (2026-06-29T06:39:03Z) - Reasoning Quality Emerges Early: Data Curation for Reasoning Models [58.56882815783977]
我々は,初期推論トークンのみを用いて,多種多様かつ挑戦的な推論例を識別可能であることを示す。
本手法は,トークン効率を91%向上させながら,既存のベースラインを最大1.7%向上させる。
論文 参考訳（メタデータ） (2026-06-25T09:32:58Z) - Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
シャノン型エントロピーの不等式を証明することは情報理論の基本的な課題である。
我々は,原子実証のステップを微調整した小規模大規模言語モデルがこのプロセスを自動化することができるか検討する。
GPT-5.5は0ショットプロンプトで1.7%のサンプルを解き、Psitipは33.3%のサンプルを解いた。
論文 参考訳（メタデータ） (2026-06-04T05:43:12Z) - FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks [0.0]
MathCheckのパラフレーズ品質検査では, 19群で4つの意味的不正確なパラフレーズが検出された。
GPT-4oは2位から4位へと降格し、クロード・ハイクとディープ・シークV3が上昇する。
論文 参考訳（メタデータ） (2026-05-27T18:59:18Z) - Let the Results Speak: A Replication-First Paradigm for LLM Behavioral Benchmarking [22.825786049667602]
本稿では,1つのヒト・ラタのコンセンサスに有効性を確保するために,複製第一パラダイムを提案する。
楽器を4つの特性で認証する - Kランの信頼性、アーキテクチャ的に異なる審査員間のクロスインストラクトレプリケーション、以前のトレーニングコホートからの審査員による歴史的フットプリントキャリブレーション、事前登録された予測。
本研究は, 自己発達型データ駆動による情緒的伴奏で, 次元は事前に決められず, 手順は9次元に安定化する。
論文 参考訳（メタデータ） (2026-05-27T03:41:11Z) - Uncovering the Representation Geometry of Minimal Cores in Overcomplete Reasoning Traces [56.497263592610295]
言語モデルは、しばしば長いチェーン・オブ・ソート・トレースを生成するが、最終的な予測を維持するのに、この理由がどの程度必要かは定かではない。
オーバーコンプリート推論トレースのレンズを通してこれを研究する。
我々は最小のコアを最終回答または予測分布を保存するステップの最小サブセットとして定義する。
論文 参考訳（メタデータ） (2026-05-14T04:35:45Z) - Measuring Faithfulness Depends on How You Measure: Classifier Sensitivity in LLM Chain-of-Thought Evaluation [0.0]
連鎖忠実性に関する最近の研究は、単一集合数について報告している。
本論文は、忠実性はモデルの客観的かつ測定可能な性質ではないことを示す。
論文 参考訳（メタデータ） (2026-03-20T17:48:43Z) - Causal Understanding by LLMs: The Role of Uncertainty [43.87879175532034]
近年の論文では、LLMは因果関係分類においてほぼランダムな精度を達成している。
因果的事例への事前曝露が因果的理解を改善するか否かを検討する。
論文 参考訳（メタデータ） (2025-09-24T13:06:35Z) - Benchmarking Reasoning Robustness in Large Language Models [76.79744000300363]
新規データや不完全データでは,性能が著しく低下することがわかった。
これらの結果は、厳密な論理的推論に対するリコールへの依存を浮き彫りにした。
本稿では,情報不足によって引き起こされる幻覚を利用して推論ギャップを明らかにする,Math-RoBと呼ばれる新しいベンチマークを提案する。
論文 参考訳（メタデータ） (2025-03-06T15:36:06Z) - Faithful Chain-of-Thought Reasoning [51.21714389639417]
CoT(Chain-of-Thought)は言語モデル(LM)のパフォーマンスを様々な推論タスクで向上させる。
翻訳と問題解決という2つの段階を含む推論フレームワークであるFithful CoTを提案する。
このことは、推論連鎖が最終回答の忠実な説明を提供することを保証している。
論文 参考訳（メタデータ） (2023-01-31T03:04:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。