Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Markets

• URL: http://arxiv.org/abs/2102.03044v2
• Date: Mon, 8 Feb 2021 09:17:06 GMT
• Title: Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Markets
• Abstract summary: SPRIG allows agents to propose and verify succinct and informative proofs in a decentralized fashion. We show how agents with various types of information interact, leading to a proof tree with an appropriate level of detail. We then analyze a simplified model, characterize its equilibria and compute the agents' level of trust.
• Score: 4.567122178196833
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modern mathematics is built on the idea that proofs should be translatable into formal proofs, whose validity is an objective question, decidable by a computer. Yet, in practice, proofs are informal and may omit many details. An agent considers a proof valid if they trust that it could be expanded into a machine-verifiable proof. A proof's validity can thus become a subjective matter and lead to a debate, which may be difficult to settle. Hence, while the concept of valid proof is well-defined, the process to establish validity is itself a complex multi-agent problem. We introduce the SPRIG protocol. SPRIG allows agents to propose and verify succinct and informative proofs in a decentralized fashion; the trust is established by agents being able to request more details in the proof steps; debates, if they arise, must isolate details of proofs and, if they persist, go down to machine-level details, where they are automatically settled. A structure of bounties and stakes is set to incentivize agents to act in good faith. We propose a game-theoretic discussion of SPRIG, showing how agents with various types of information interact, leading to a proof tree with an appropriate level of detail and to the invalidation of wrong proofs, and we discuss resilience against various attacks. We then analyze a simplified model, characterize its equilibria and compute the agents' level of trust. SPRIG is designed to run as a smart contract on a blockchain platform. This allows anonymous agents to participate in the verification debate, and to contribute with their information. The smart contract mediates the interactions, settles debates, and guarantees that bounties and stakes are paid as specified. SPRIG enables new applications, such as the issuance of bounties for open problems, and the creation of derivatives markets, allowing agents to inject more information pertaining to proofs.

Related papers

• Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
  Multi-agent AI platforms move quickly from staging to production, but the way agents establish trust remains rudimentary.<n>We take provable data minimisation between agents from proposal to running system.<n>A 32-bit threshold predicate proves in 6.2 ms and verifies in 1.0 ms with a 608-byte Bulletproofs proof.
  arXiv  Detail & Related papers  (2026-08-30T23:16:17Z)
• Prove2Me: An Open Collaborative Platform for Scaling Math Formalization [5.249471979820288]
  We introduce Prove2Me, an open collaborative platform for formalizing mathematics.<n>Users launch formalization "missions", to which AI agents contribute formal proofs toward completion.<n>In doing so, Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent.
  arXiv  Detail & Related papers  (2026-08-28T15:16:25Z)
• HypoAgent: An Agentic Framework for Interactive Abductive Hypothesis Generation over Knowledge Graphs [52.91976391891331]
  Abductive reasoning over knowledge graphs aims to generate logical hypotheses that explain observed entities or facts.<n>Existing controllable hypothesis generation methods allow users to guide this process with explicit conditions.<n>We propose HypoAgent, an Agentic framework for interactive abductive Hypothesis Generation over knowledge graphs.
  arXiv  Detail & Related papers  (2026-05-29T14:40:37Z)
• AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
  Verifiers have been demonstrated to enhance LLM reasoning via test-time scaling (TTS)<n>We propose Agentic Verifier, a framework that transforms reward modeling into a multi-turn, tool-augmented deliberative process.<n>We show that Agentic Verifier yields consistent performance gains under both parallel and sequential TTS.
  arXiv  Detail & Related papers  (2026-04-17T12:27:36Z)
• Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents [2.8292841621378844]
  This setting explores collaborative, decentralized proof search and theory building.<n>Agents interact directly with the interactive proof system.<n>All accepted proofs are checked and verified by the underlying proof assistant.
  arXiv  Detail & Related papers  (2026-03-06T07:34:07Z)
• Protocol Agent: What If Agents Could Use Cryptography In Everyday Life? [0.0]
  We show how agents could develop communication patterns that are more efficient and better aligned with their capabilities.<n> cryptographic primitives that could profoundly improve everyday interactions already exist, but humans can't use them because they are too complex and the math can't be done in one's head.<n>What if agents could create protocols "on the fly" by recognizing which primitive fits an everyday situation, proposing it to an agentic counterpart, persuading them to participate, and then executing the protocol correctly using appropriate computation tools?<n>We evaluate current open-weight and state-of-the-art models on this benchmark, propose
  arXiv  Detail & Related papers  (2026-02-01T16:05:35Z)
• Towards Automating Blockchain Consensus Verification with IsabeLLM [1.9336815376402718]
  We present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs.<n>We demonstrate the effectiveness of IsabeLLM by using it to develop a novel model of Bitcoin's Proof of Work consensus protocol and verify its correctness.
  arXiv  Detail & Related papers  (2026-01-12T15:35:08Z)
• SmartSnap: Proactive Evidence Seeking for Self-Verifying Agents [45.71333459905404]
  SmartSnap is a paradigm shift from passive, post-hoc verification to proactive, in-situ self-verification by the agent itself.<n>We introduce the Self-Verifying Agent, a new type of agent designed with dual missions: to complete a task and to prove its accomplishment with curated evidences.<n>Experiments on mobile tasks across model families and scales demonstrate that our SmartSnap paradigm allows training LLM-driven agents in a scalable manner.
  arXiv  Detail & Related papers  (2025-12-26T14:51:39Z)
• Inter-Agent Trust Models: A Comparative Study of Brief, Claim, Proof, Stake, Reputation and Constraint in Agentic Web Protocol Design-A2A, AP2, ERC-8004, and Beyond [1.5755923640031846]
  We study trust models in inter-agent protocol design.<n>We analyze assumptions, attack surfaces, and design trade-offs.<n>We distill actionable design guidelines for safer, interoperable, and scalable agent economies.
  arXiv  Detail & Related papers  (2025-11-05T12:50:06Z)
• When Agents Trade: Live Multi-Market Trading Benchmark for LLM Agents [74.55061622246824]
  Agent Market Arena (AMA) is the first lifelong, real-time benchmark for evaluating Large Language Model (LLM)-based trading agents.<n>AMA integrates verified trading data, expert-checked news, and diverse agent architectures within a unified trading framework.<n>It evaluates agents across GPT-4o, GPT-4.1, Claude-3.5-haiku, Claude-sonnet-4, and Gemini-2.0-flash.
  arXiv  Detail & Related papers  (2025-10-13T17:54:09Z)
• What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
  We conduct a user study involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages.<n>Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process.<n>We translate these findings into concrete design guidance for AI proof assistants.
  arXiv  Detail & Related papers  (2025-08-01T22:16:30Z)
• Operator: A Protocol for Trustless Delegation Under Uncertainty [0.0]
  We propose a protocol that enforces correctness through collateralized claims in a verification game.<n>Tasks are published as intents, and solvers compete to fulfill them.<n>Any challenger can challenge a result by staking against it to trigger the verification process.<n>Incorrect agents are slashed and correct opposition is rewarded, with an escalation path that penalizes erroneous verifiers themselves.
  arXiv  Detail & Related papers  (2025-07-01T10:22:35Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Agent TCP/IP: An Agent-to-Agent Transaction System [0.0]
  Agent Transaction Control Protocol for Intellectual Property introduces a trustless framework for exchanging IP between agents. Agents can initiate, trade, borrow, and sell agent-to-agent contracts on the Story blockchain network. Agents can autonomously sell their training data to other agents, license confidential or proprietary information, collaborate on content based on their unique skills.
  arXiv  Detail & Related papers  (2025-01-08T16:43:47Z)
• Towards Secure and Trusted-by-Design Smart Contracts [0.3499870393443268]
  Evidential transactions involve the exchange of any form of physical evidence, such as money, birth certificate, visas, tickets, etc. Most of the time, evidential transactions occur in the context of complex procedures, called evidential protocols, among physical agents. The blockchain provides the mechanisms to transfer evidence, while smart contracts allow encoding evidential protocols on top of a blockchain. As a smart contract foregoes trusted third-parties and runs on several machines anonymously, it constitutes a highly critical program that has to be secure and trusted-by-design.
  arXiv  Detail & Related papers  (2024-03-25T16:14:22Z)
• Unclonable Non-Interactive Zero-Knowledge [11.013799869152132]
  A non-interactive ZK (NIZK) proof enables verification of NP statements without revealing secrets about them. In this paper, we ask whether it is possible to rely on quantum information in order to build NIZK proof systems that are impossible to clone.
  arXiv  Detail & Related papers  (2023-10-11T01:32:36Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• Fact-Saboteurs: A Taxonomy of Evidence Manipulation Attacks against Fact-Verification Systems [80.3811072650087]
  We show that it is possible to subtly modify claim-salient snippets in the evidence and generate diverse and claim-aligned evidence. The attacks are also robust against post-hoc modifications of the claim. These attacks can have harmful implications on the inspectable and human-in-the-loop usage scenarios.
  arXiv  Detail & Related papers  (2022-09-07T13:39:24Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Synthetic Disinformation Attacks on Automated Fact Verification Systems [53.011635547834025]
  We explore the sensitivity of automated fact-checkers to synthetic adversarial evidence in two simulated settings. We show that these systems suffer significant performance drops against these attacks. We discuss the growing threat of modern NLG systems as generators of disinformation.
  arXiv  Detail & Related papers  (2022-02-18T19:01:01Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)
• Experimental relativistic zero-knowledge proofs [4.334542470441071]
  We develop a zero-knowledge protocol involving two separated verifier-prover pairs. Security is enforced via the physical principle of special relativity. This demonstrates the practical potential of multi-prover zero-knowledge protocols.
  arXiv  Detail & Related papers  (2020-12-18T19:00:01Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)
• Empirically Verifying Hypotheses Using Reinforcement Learning [58.09414653169534]
  This paper formulates hypothesis verification as an RL problem. We aim to build an agent that, given a hypothesis about the dynamics of the world, can take actions to generate observations which can help predict whether the hypothesis is true or false.
  arXiv  Detail & Related papers  (2020-06-29T01:01:10Z)
• SNARKs to the rescue: proof-of-contact in zero knowledge [0.0]
  This paper describes techniques to help with COVID-19 automated contact tracing, and with the restoration efforts. We describe a decentralized protocol for proof-of-contact'' in zero knowledge where a person can publish a short cryptographic proof attesting to the fact that they have been infected.
  arXiv  Detail & Related papers  (2020-05-26T13:00:37Z)

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.