A First Proof Sprint

• URL: http://arxiv.org/abs/2602.13587v1
• Date: Sat, 14 Feb 2026 04:09:30 GMT
• Title: A First Proof Sprint
• Abstract summary: This monograph reports a multi-agent proof sprint on ten research-level problems.<n>Problem3 has a validation-complete existence path under the scoped criterion used here.<n>Problem5 is solved in a scope-limited form for $F_O$-local connective spectra.<n>Problem6 is partial with named remaining obligations in the general case.<n>Problem7 and9 have node-level validation artifacts but still contain unresolved verifier gaps.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This monograph reports a multi-agent proof sprint on ten research-level problems, combining rapid draft generation with adversarial verification, targeted repair, and explicit provenance. The workflow uses wiring-diagram decompositions of claim dependencies to localize gaps and coordinate reviewer-driven revisions. Final outcomes are heterogeneous but explicit: the manuscript distinguishes mathematical status from QC-validation status. Mathematically, Problem~3 has a validation-complete existence path under the scoped criterion used here (uniqueness/irreducibility treated as optional), Problem 5 is solved in a scope-limited form for $F_O$-local connective spectra, Problem 10 is conditional under clearly stated assumptions (with explicit necessity counterexamples when assumptions are dropped), and Problems 4 and 6 are partial with named remaining obligations in the general case (including an unconditional $K_n$ result for Problem 6 with $c_0 = 1/3$). Problem 7 is treated as provisionally closed via the rotation-route theorem chain, pending independent ledger re-check. At the QC layer, Problems~7 and~9 have node-level validation artifacts but still contain unresolved verifier gaps. The main methodological result is that structure-aware verification and layer-switching strategies improve reliability and calibration in compressed proof sprints.

Related papers

• LEDGERMIND: Provenance-Constrained Multimodal Agentic Reasoning with a Structured Evidence Ledger [11.70343232168598]
  LedgerMind is a provenance-constrained agentic reasoning engine.<n>It targets four recurring failure patterns that final-answer accuracy tends to obscure.<n>It improves both answer accuracy and trajectory-level faithfulness.
  arXiv  Detail & Related papers  (2026-07-30T15:35:34Z)
• Interventional Grounding Audits: Black-Box Premise-Dependency Tests for LLM Chain-of-Thought via Predicate Substitution [0.0]
  Large language models produce chain-of-thought (CoT) reasoning that appears logically sound yet may not genuinely depend on its stated premises.<n>We introduce interventional grounding audits, a black-box, step-level test of premise dependency.<n>All audit certificates, raw outputs, and reproduction scripts are available in a public GitHub repository.
  arXiv  Detail & Related papers  (2026-07-11T01:32:22Z)
• NormWorlds-CF: Solver-Verified Counterfactual Normative Reasoning with Metamorphic-Relation GRPO [1.5483078145498086]
  NormWorlds-CF is a solver-verified environment for counterfactual normative reasoning in rule worlds.<n>Its deterministic solver produces final answers, proof and falsification certificates, argument statuses, support sets, and paired-world change labels.
  arXiv  Detail & Related papers  (2026-07-04T17:11:21Z)
• Affordance Agent Harness: Verification-Gated Skill Orchestration [45.231685718099264]
  Affordance grounding requires identifying where and how an agent should interact in open-world scenes.<n>We propose Affordance Agent Harness, a closed-loop runtime that unifies skills with an evidence store and cost control.
  arXiv  Detail & Related papers  (2026-05-01T13:45:16Z)
• IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
  Existing pipelines produce opaque, end-to-end outputs that expose no intermediate state for inspection.<n>We present IMPACT-Cycle, a supervisory multi-agent system that reformulates long-video understanding as a multimodal iterative claim-level maintenance.
  arXiv  Detail & Related papers  (2026-04-22T03:03:33Z)
• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  We propose a paired-outcome measurement interface for auditing a single protocol step on exact-match tasks.<n>For each instance, the interface records a baseline correctness bit and a post-step correctness bit.<n>These rates predict accuracy changes and define a reusable empirical interface testable across seeds, mixtures, and pipelines.
  arXiv  Detail & Related papers  (2026-04-20T13:25:40Z)
• zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing [7.274627641804014]
  zkCraft is a framework that combines deterministic, R1CS-aware localization with proof-bearing search to detect semantic inconsistencies.<n>We show that proof-bearing localization detects diverse under- and over-constrained faults with low false positives and reduces costly solver interaction.
  arXiv  Detail & Related papers  (2026-01-31T11:31:00Z)
• CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
  Group-relative reinforcement learning with verifiable rewards (RLVR) often wastes the most informative data it already has the failures.<n>We present CARE, a failure-centric post-training framework for multimodal reasoning that turns errors into supervision.<n> CARE improves accuracy and training smoothness while explicitly increasing the share of learning signal that comes from failures.
  arXiv  Detail & Related papers  (2025-12-22T16:34:21Z)
• The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
  This work bridges the gap by developing an LLM-Verifier Convergence Theorem.<n>We model the interaction between the LLM and the verifier as a discrete-time Markov Chain.<n>We stress-tested this prediction in an extensive empirical campaign comprising more than 90,000 trials.
  arXiv  Detail & Related papers  (2025-11-30T22:19:09Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Evidence-Bound Autonomous Research (EviBound): A Governance Framework for Eliminating False Claims [0.609170287691728]
  EviBound is an evidence-bound execution framework that eliminates false claims through dual governance gates.<n>The pre-execution Approval Gate validates acceptance criteria schemas before code runs.<n>The post-execution Verification Gate validates artifacts via MLflow API queries.
  arXiv  Detail & Related papers  (2025-10-28T17:47:13Z)
• Hierarchical Sequence Iteration for Heterogeneous Question Answering [27.22775290181187]
  This paper introduces HSEQ, a unified framework that linearizes documents, tables, and knowledge graphs into a reversible hierarchical sequence.<n> Experiments on HotpotQA (text), HybridQA/TAT-QA (table+text), and MetaQA (KG) show consistent EM/F1 gains over strong single-pass, multi-hop, and agentic RAG baselines with high efficiency.
  arXiv  Detail & Related papers  (2025-10-23T12:48:18Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  We develop a unified framework that combines implicit retrieval and structured collaboration.<n>On Humanity's Last Exam (HLE) Bio/Chem Gold, our framework achieves 48.3% accuracy.<n>Results on SuperGPQA and TRQA confirm robustness across domains.
  arXiv  Detail & Related papers  (2025-09-25T14:05:55Z)
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees [8.804277530769532]
  State-of-the-art, branch and bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better.<n>We propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples.<n>Oliva has two variants, including $OlivaGR$, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples.
  arXiv  Detail & Related papers  (2025-07-23T12:20:20Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  We introduce Veracity Search (VS), a discrete search algorithm over veracity assignments.<n>It performs otherwise intractable inference in the posterior distribution over latent veracity values.<n>It generalizes VS, enabling accurate zero-shot veracity inference in novel contexts.
  arXiv  Detail & Related papers  (2025-05-17T04:16:36Z)
• RCOT: Detecting and Rectifying Factual Inconsistency in Reasoning by Reversing Chain-of-Thought [56.558892336235914]
  Reversing Chain-of-Thought (RCoT) is a novel method to improve large language models' reasoning abilities. RCoT automatically detects and rectifys factual inconsistency in generated solutions. We show that manually written fine-grained feedback can dramatically improve LLMs' reasoning abilities.
  arXiv  Detail & Related papers  (2023-05-19T08:02:52Z)
• 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)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)

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.