Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

Chad E. Brown, Cezary Kaliszyk, Josef Urban

TL;DR

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 and a simulated bounty-based marketplace is implemented.

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.

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

TL;DR

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 and a simulated bounty-based marketplace is implemented.

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.
Paper Structure (8 sections, 2 figures, 1 table)

This paper contains 8 sections, 2 figures, 1 table.

Table of Contents

  1. Motivation: Fast Parallelized LLM Autoformalization
  2. Target: Autoformalization of Algebraic Topology in Megalodon
  3. Initial Autoformalization of Statements and Setting of Bounties
  4. Agent and Bounty Based Setup
  5. Formalization Growth and Collaborative Aspects
  6. Observations and Remarks
  7. Megalodon Changes
  8. Major Theorems Proved and Case Studies

Figures (2)

  • Figure 1: Growth of the formalization over history (commit numbers).
  • Figure 2: History of balances, locks, bounty collection and placement (over commit numbers), the line for Charlie has been reset at balance-reset point as discussed in Sect. \ref{['s:charliecheat']}.