PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs

• URL: http://arxiv.org/abs/2607.16997v1
• Date: Sat, 18 Jul 2026 23:10:00 GMT
• Title: PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs
• Abstract summary: We study a deliberately narrower construct: time-relative proof-route nonstandardness in formal mathematics.<n>PriorProof extracts the dependency footprint of its elaborated proof term and scores the weighted surprisal of that footprint.<n>We present PriorProof as a decomposable, time-anchored signal whose score gap provides an interpretable reliability indicator.
• Score: 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.

Related papers

• Marginal Fidelity Does Not Establish User Simulation in Demographic Synthetic Survey Panels: Response Contracts, Support Collapse and Conditioning Failure [51.736723807086385]
  Population-marginal agreement is evidence about an elicitation contract and an estimand obtainable without simulated respondents, not evidence of individual simulation.<n>On nine aligned model-battery pairs, a no-persona population-prevalence query averages 6.27 MAE versus 12.39 for committed panels and wins all nine comparisons.
  arXiv  Detail & Related papers  (2026-09-07T10:22:22Z)
• Reliable Benchmarking of Artifact Detection in Computational Pathology: A Reproducibility and Uncertainty Analysis [1.8864137667201766]
  Methods: The protocol quantifies four sources of variability - test-set sampling, trainingity, partition composition, and undocumented preprocessing.<n>We apply it to an independent reconstruction of a published diffusion-based artifact detector, evaluated on the original 24-slide partition and against a supervised baseline.<n>Results: The method's central mechanism reproduces: the auxiliary contrastive term improves pooled F1 from 0.673 to 0.688 and replicates under a second seed.
  arXiv  Detail & Related papers  (2026-08-31T14:07:15Z)
• Agreement Before Diversity: Verification-First Complementarity for Heterogeneous Language-Model Coordination [11.215813718564283]
  We decouple candidate headroom from replacement authority, rendering the latter as an explicit, auditable object.<n>Our proposed method, Agreement-Before-Diversity, is a frozen, label-free decision rule.
  arXiv  Detail & Related papers  (2026-08-05T09:24:39Z)
• Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
  We describe our PointArena 2026 solution, which achieves 77.2% overall accuracy and ranks second on the benchmark.<n>The ap proach targets three failure modes. First, agent-driven syn thesis builds large semantic and anchor-relative candidate pools.<n>Second, a determinis tic steerable-data pipeline creates a verified 10,000-sample main set, plus reserve samples, using masks, templates, and path verification.
  arXiv  Detail & Related papers  (2026-06-29T06:39:03Z)
• Reasoning Quality Emerges Early: Data Curation for Reasoning Models [58.56882815783977]
  We show that diverse and challenging reasoning examples can be identified using only the initial reasoning tokens.<n>Our method outperforms existing baselines by up to 1.7% while being 91% more token efficient.
  arXiv  Detail & Related papers  (2026-06-25T09:32:58Z)
• Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
  Proving Shannon-type entropy inequalities is a fundamental task in information theory.<n>We investigate whether small-scale large language models, fine-tuned on atomic proof steps, can automate this process.<n>We show that GPT-5.5 solves 1.7% samples under zero-shot prompting while Psitip solves 33.3% samples.
  arXiv  Detail & Related papers  (2026-06-04T05:43:12Z)
• FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks [0.0]
  A paraphrase-quality audit of MathCheck detected 4 semantically incorrect paraphrases in 129 groups.<n>Removing them drops GPT-4o from rank 2 to rank 4 and elevates Claude Haiku and DeepSeek V3 above it.
  arXiv  Detail & Related papers  (2026-05-27T18:59:18Z)
• Let the Results Speak: A Replication-First Paradigm for LLM Behavioral Benchmarking [22.825786049667602]
  We propose a replication-first paradigm to anchor validity to a single human-rater consensus.<n>We certify the instrument via four properties -- reliability across K runs, cross-instrument replication across architecturally distinct judges, historical-footprint calibration via judges from earlier training cohorts, and pre-registered prediction.<n>We test it on emotional accompaniment by letting the self-evolve data-driven across: the dimensions are not pre-stipulated and the procedure stabilizes to a 9-dimension set.
  arXiv  Detail & Related papers  (2026-05-27T03:41:11Z)
• Uncovering the Representation Geometry of Minimal Cores in Overcomplete Reasoning Traces [56.497263592610295]
  Language models often generate long chain-of-thought traces, but it remains unclear how much of this reasoning is necessary for preserving the final prediction.<n>We study this through the lens of overcomplete reasoning traces.<n>We define the minimal core as the smallest subset of steps that preserves either the final answer or predictive distribution.
  arXiv  Detail & Related papers  (2026-05-14T04:35:45Z)
• Measuring Faithfulness Depends on How You Measure: Classifier Sensitivity in LLM Chain-of-Thought Evaluation [0.0]
  Recent work on chain-of-thought faithfulness reports single aggregate numbers.<n>This paper provides evidence that faithfulness is not an objective, measurable property of a model.
  arXiv  Detail & Related papers  (2026-03-20T17:48:43Z)
• Causal Understanding by LLMs: The Role of Uncertainty [43.87879175532034]
  Recent papers show LLMs achieve near-random accuracy in causal relation classification.<n>We investigate whether pretraining exposure to causal examples improves causal understanding.
  arXiv  Detail & Related papers  (2025-09-24T13:06:35Z)
• Benchmarking Reasoning Robustness in Large Language Models [76.79744000300363]
  We find significant performance degradation on novel or incomplete data.<n>These findings highlight the reliance on recall over rigorous logical inference.<n>This paper introduces a novel benchmark, termed as Math-RoB, that exploits hallucinations triggered by missing information to expose reasoning gaps.
  arXiv  Detail & Related papers  (2025-03-06T15:36:06Z)
• Faithful Chain-of-Thought Reasoning [51.21714389639417]
  Chain-of-Thought (CoT) prompting boosts Language Models' (LM) performance on a gamut of reasoning tasks. We propose Faithful CoT, a reasoning framework involving two stages: Translation and Problem Solving. This guarantees that the reasoning chain provides a faithful explanation of the final answer.
  arXiv  Detail & Related papers  (2023-01-31T03:04:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.