Cogentic：面向自动证明发现的多智能体编排架构解析

Single-shot LLM generation breaks down on open research problems. You need to explore competing conjectures, overcome technical obstructions, and retain intermediate progress over long horizons. Cogentic is a multi-agent harness that solves this coordination problem for automated theorem proving. It produced novel results on five open problems in online learning, auction theory, and mechanism design using Gemini as the base model.

The architecture exposes orchestration patterns that apply beyond math: how to spawn agents across distinct proof directions, when to promote intermediate results into shared state, and how to prune the search space when competing hypotheses explode.

The Coordination Problem

Research-grade tasks require more than chaining tool calls. You need:

• Parallel exploration of multiple competing approaches without duplicating work
• Adversarial verification to catch subtle errors before they propagate
• Persistent state that survives agent handoffs and long proof attempts
• Dynamic allocation that shifts compute toward promising branches

Single-agent workflows fail because they commit too early. Multi-agent systems without coordination waste compute on redundant paths or lose intermediate progress when agents disagree on lemmas.

Architecture: Prove-Verify Loop

Cogentic runs an iterative loop with three layers:

1. Orchestrator: Allocates a population of independent provers across distinct proof directions
2. Prover agents: Generate proof attempts in parallel, each exploring a different conjecture or technical approach
3. Verification layer: Adversarial components check each proof attempt and promote confirmed results to a verified ledger

The verified ledger is the critical piece. It acts as a shared knowledge base that later rounds build on. Agents read from the ledger to avoid re-proving known results and write to it only after passing verification.

State Synchronization

Each prover operates independently but reads from a shared ledger before starting work. This prevents duplication:

• Prover checks ledger for existing results on subproblem X
• If X is already verified, prover skips it and moves to the next branch
• If X is unverified, prover attempts a proof and submits to verification

The orchestrator tracks which subproblems are currently being attempted to avoid assigning the same work to multiple agents. This is a simple lock mechanism: when a prover claims a subproblem, it gets marked as "in progress" until the prover either succeeds or times out.

Verification as a Gatekeeper

Verification is adversarial. Multiple specialized components review each proof attempt:

• Formal checker: Validates logical steps against known axioms
• Counterexample generator: Tries to break the proof with edge cases
• Domain critic: Checks for subtle technical errors specific to the problem domain

Only proofs that pass all three gates get written to the ledger. This prevents cascading failures where one bad lemma poisons downstream work.

Exploration vs. Exploitation

The orchestrator decides when to spawn new agents and when to double down on existing branches. It uses a simple heuristic:

• Exploration: If no branch has produced verified results in N rounds, spawn agents on new conjectures
• Exploitation: If a branch produces verified lemmas, allocate more agents to extend that branch

This is a greedy strategy with a timeout. If exploitation stalls (no new verified results after M rounds), the orchestrator switches back to exploration.

Pruning the Search Space

When competing hypotheses explode, the orchestrator prunes branches based on:

• Verification rate: Branches with low verification rates get deprioritized
• Ledger dependencies: Branches that depend on unverified lemmas get paused until dependencies resolve
• Compute budget: Hard limit on total active provers

Pruning is conservative. The orchestrator never kills a branch permanently, it just deprioritizes it. If other branches stall, pruned branches can be revived.

Failure Modes

Agent Disagreement on Lemmas

When two agents propose conflicting lemmas, the verification layer catches it. The orchestrator then:

1. Marks both lemmas as "disputed"
2. Spawns a dedicated agent to resolve the conflict
3. Pauses downstream work that depends on either lemma

This creates a temporary bottleneck but prevents bad state from propagating.

Verification Bottleneck

If verification is slow, provers queue up waiting for results. The orchestrator monitors queue depth and throttles prover allocation when the queue exceeds a threshold. This is a backpressure mechanism: slow down generation when verification can't keep up.

Infinite Exploration

Without pruning, the orchestrator can spawn agents indefinitely on unproductive branches. The compute budget acts as a hard stop, but it's a blunt instrument. Better heuristics would track the marginal value of each branch (verified results per agent-hour) and kill branches with declining returns.

Instrumentation and Observability

Debugging multi-agent proof attempts requires visibility into:

• Branch genealogy: Which lemmas depend on which prior results
• Verification history: Why proofs failed and which component rejected them
• Agent utilization: How much time agents spend waiting vs. proving

Cogentic logs all of this to a structured event stream. Each event includes:

{
  "timestamp": "2026-09-30T17:55:22Z",
  "agent_id": "prover-42",
  "event_type": "proof_attempt",
  "subproblem": "lemma-3.2",
  "dependencies": ["lemma-2.1", "lemma-2.5"],
  "verification_result": "rejected",
  "rejection_reason": "counterexample_found",
  "compute_time_ms": 12400
}

This lets you replay proof attempts and understand why certain branches succeeded or failed.

Deployment Shape

Cogentic runs on a cluster of GPU instances with:

• Orchestrator: Single stateful process that manages the ledger and allocates work
• Prover pool: N stateless workers that pull tasks from a queue
• Verification cluster: M specialized workers for formal checking, counterexample generation, and domain critique

The orchestrator is the single point of failure. If it crashes, you lose in-flight state but the ledger persists. Provers and verifiers are stateless and can be scaled independently.

Cost Profile

Research-grade proof discovery is expensive. Cogentic's five novel results required:

• Hundreds of prover-hours per problem
• Multiple rounds of exploration and pruning
• Human expert verification of final results

This is not a real-time system. Proof attempts run for hours or days. The orchestrator checkpoints the ledger periodically so you can resume after failures.

Trade-offs

When Competing Hypotheses Collide

The hardest failure mode is when two branches produce conflicting verified lemmas. This shouldn't happen if verification is sound, but it can occur when:

• Verification components have bugs
• Domain critics miss subtle errors
• Formal checkers use incomplete axiom sets

Cogentic's solution is to escalate to human review. The orchestrator flags the conflict, pauses all dependent work, and waits for a human expert to resolve it. This is a manual escape hatch, not an automated recovery mechanism.

Technical Verdict

Use Cogentic's patterns when:

• You need to explore multiple competing approaches in parallel
• Intermediate results must be verified before downstream work depends on them
• The search space is too large for exhaustive exploration
• You can tolerate long runtimes (hours to days)

Avoid this architecture when:

• You need real-time or near-real-time results
• Single-shot generation is sufficient (most tasks)
• You can't afford the coordination overhead of a persistent ledger
• Verification is too expensive or slow to gate every intermediate result

The core insight is that research-grade tasks need a different orchestration model than typical agent workflows. You can't chain tool calls and hope for the best. You need parallel exploration, adversarial verification, and a shared knowledge base that survives agent handoffs. That's expensive infrastructure, but it's the only way to solve open problems that require exploring multiple dead ends before finding a proof.

Source Links

• Cogentic: Multi-Agent Orchestration for Automated Proof Discovery (ArXiv)
• PDF