Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

• URL: http://arxiv.org/abs/2603.06737v1
• Date: Fri, 06 Mar 2026 07:34:07 GMT
• Title: Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
• Abstract summary: 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.
• Score: 2.8292841621378844
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multiple LLM-based coding agents. Rather than relying on static central planning, we implement a simulated bounty-based marketplace in which agents dynamically propose new lemmas (formal statements), attach bounties to them, and compete to discharge these proof obligations and claim the bounties. The agents interact directly with the interactive proof system: they can invoke tactics, inspect proof states and goals, analyze tactic successes and failures, and iteratively refine their proof scripts. In addition to constructing proofs, agents may introduce new formal definitions and intermediate lemmas to structure the development. All accepted proofs are ultimately checked and verified by the underlying proof assistant. This setting explores collaborative, decentralized proof search and theory building, and the use of market-inspired mechanisms to scale autoformalization in ITP.

Related papers

• (Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs [0.20305676256390937]
  We present an autoformalization system that leverages LLM agents in a deterministically constrained workflow to enforce incremental progress in Lean autoformalization tasks.<n>Our approach is motivated by the common mathematician's notion of what it means to have a rigorous proof in the first place.<n>We link to an end-to-end Lean formalization of a recent Ramsey theory breakthrough produced by the process.
  arXiv  Detail & Related papers  (2026-06-08T15:57:14Z)
• A Sober Look at Agentic Misalignment in Automated Workflows [39.62671225833463]
  We study a class of emergent misalignment in multi-agent systems (MAS)<n>Agentic Evidence Attribution (AEA) is a novel alignment paradigm that improves agent posteriors using context-specific evidence.
  arXiv  Detail & Related papers  (2026-05-22T20:40:20Z)
• VerifyMAS: Hypothesis Verification for Failure Attribution in LLM Multi-Agent Systems [79.51005192758262]
  Large language model-driven multi-agent systems excel at complex tasks.<n>However, unreliable agents remain a key bottleneck to system-level reliability.<n>We propose a hypothesis verification framework for agent failure attribution.
  arXiv  Detail & Related papers  (2026-05-17T14:09:35Z)
• Beyond Individual Intelligence: Surveying Collaboration, Failure Attribution, and Self-Evolution in LLM-based Multi-Agent Systems [65.90791804095561]
  Multi-agent systems address this through structured collaboration among specialized agents, but tighter coordination amplifies a less explored risk.<n>Existing surveys cover individual agent capabilities, multi-agent collaboration, or agent self-evolution separately, leaving the causal dependencies among them unexamined.<n>This survey provides a unified review organized around four causally linked stages, which we term the LIFE progression: Lay the capability foundation, Integrate agents through collaboration, Find faults through attribution, and Evolve through autonomous self-improvement.
  arXiv  Detail & Related papers  (2026-05-14T14:36:13Z)
• 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)
• Agentic Program Verification [14.684859166069012]
  We present a first Large Language Models agent, AutoRocq, for conducting program verification.<n>Unlike past works, which rely on extensive training of LLMs on proof examples, our agent learns on-the-fly and improves the proof via an iterative refinement loop.<n>In this way, our proof construction involves autonomous collaboration between the proof agent and the theorem prover.
  arXiv  Detail & Related papers  (2025-11-21T15:51:48Z)
• Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
  We present ALITA-G, a framework that transforms a general-purpose agent into a domain expert.<n>In this framework, a generalist agent executes a curated suite of target-domain tasks.<n>It attains strong gains while reducing computation costs.
  arXiv  Detail & Related papers  (2025-10-27T17:59:14Z)
• Towards Self-Evolving Benchmarks: Synthesizing Agent Trajectories via Test-Time Exploration under Validate-by-Reproduce Paradigm [60.36837655498119]
  We propose a Trajectory-based validated-by-Reproducing Agent-benchmark Complexity Evolution framework.<n>This framework takes an original task from an existing benchmark and encourages agents to evolve it into a new task with higher difficulty.<n>Experiments on the GAIA benchmark demonstrate that the TRACE framework consistently enhances task complexity while improving the reliability of correctness.
  arXiv  Detail & Related papers  (2025-10-01T01:52:52Z)
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
  We present Prover Agent, a novel AI agent for automated theorem proving.<n>It integrates large language models (LLMs) with a formal proof assistant, Lean.<n>It achieves an 88.1% success rate on the MiniF2F benchmark.
  arXiv  Detail & Related papers  (2025-06-24T18:01:52Z)
• When Disagreements Elicit Robustness: Investigating Self-Repair Capabilities under LLM Multi-Agent Disagreements [56.29265568399648]
  We argue that disagreements prevent premature consensus and expand the explored solution space.<n>Disagreements on task-critical steps can derail collaboration depending on the topology of solution paths.
  arXiv  Detail & Related papers  (2025-02-21T02:24:43Z)
• Textualized Agent-Style Reasoning for Complex Tasks by Multiple Round LLM Generation [49.27250832754313]
  We present AgentCOT, a llm-based autonomous agent framework. At each step, AgentCOT selects an action and executes it to yield an intermediate result with supporting evidence. We introduce two new strategies to enhance the performance of AgentCOT.
  arXiv  Detail & Related papers  (2024-09-19T02:20:06Z)
• Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Markets [4.567122178196833]
  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.
  arXiv  Detail & Related papers  (2021-02-05T08:00:19Z)
• 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)

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.