taocp

taocp solves and reviews exercises from The Art of Computer Programming. It is both a Go library and a command-line program.

The solver loads an exercise, relevant section text, and nearby exercises from a local TAOCP content repository. It builds a candidate-blind verification reference, generates a population of independent solutions, selects the strongest candidate obligation by obligation, then applies two independent verification prompts. A result is true only when both judges pass it. Failed results enter a bounded correction loop and are checked again from scratch.

Quality model

The workflow uses several complementary checks:

1. A private reference call solves the exercise before seeing any candidate and records obligations, likely failure modes, and falsification tests.
2. Three independent candidates are generated by default. The count is configurable from one to five.
3. A population selector checks each candidate against every obligation and the independently derived conclusion. It selects mathematical substance rather than prose polish.
4. The truth judge uses the private reference as a fallible aid and decides whether the selected answer and supporting reasoning are true, complete, self-contained, human-readable, and verifiable.
5. The reference-blind audit judge tries to falsify the selected solution with counterexamples, small and boundary cases, step checks, and an independent recomputation.
6. Both judges must pass. A disagreement, missing decision field, or material gap is false and triggers correction when correction passes remain.
7. Publication guards reject empty responses and provider leakage, normalize typography, and remove horizontal rules.

This defense-in-depth design addresses a central weakness in current mathematical verifiers: false solutions are still harder to reject than true solutions are to accept. It combines population-level generation and selection, candidate-blind reference construction, fine-grained obligation checks, explicit truth fields, and adversarial falsification. It does not treat agreement or polished style as proof of correctness.

See the live evaluation for a complete solve with both truth checks.

Install

Download a release archive or Linux package from the release page, or pull the container:

docker pull ghcr.io/tamnd/taocp-solver:latest

Install directly from source with Go:

go install github.com/tamnd/taocp-solver/cmd/taocp@latest

Building from source requires the Go version declared in go.mod:

git clone https://github.com/tamnd/taocp-solver.git
cd taocp-solver
make test build

Bridge and proxy

The default transport is streaming Chat Completions because the local subscription bridge accepts that wire format and translates it to the upstream Responses protocol. A tracing proxy can sit between taocp and the bridge without changing the solver:

taocp -> trace proxy -> local bridge -> model backend

Point --base-url at the proxy when tracing, or at the bridge when calling it directly. The URL may end at the server root or /v1.

export TAOCP_SOLVER_BASE_URL=http://localhost:8790/v1
export TAOCP_SOLVER_MODEL=gpt-5.6-sol

taocp solve 1.1 1

An API key is optional for a trusted local bridge and required when the selected endpoint requires one:

export TAOCP_SOLVER_API_KEY=your-key

Command line

Solve one exercise in slow mode, which is the default:

taocp solve 1.2.6 10
taocp solve 1.2.6.10

Use fast mode for one solution call with no verification, or select slow mode explicitly for the full population and truth harness:

taocp solve 1.2.6 10 --mode fast
taocp solve 1.2.6 10 --mode slow --candidates 3

The command prints the saved Markdown path to standard output and a compact audit summary to standard error:

verdict: PASS, truth: true, elapsed: 20m38.834s
tokens: input 34754 (uncached 34754, cached 0, cache write 0), output 49320 (reasoning 38179), total 84074 across 7 requests
official list cost estimate: $1.653370 USD

Re-solve an exercise even when a cached result exists:

taocp solve 1.2.6 10 --force

Solve every exercise in selected sections:

taocp batch 1.1 1.2.1 --parallel 2

Inspect the exact solution prompt without making a model call:

taocp prompt 1.1 1

Run both judges on an existing Markdown solution:

taocp review 1.1 1 --file solution.md

Generate fast and slow solutions for the same exercise, audit them blindly in both answer orders, and compare quality, tokens, and standard list cost:

taocp benchmark 1.1 1
taocp benchmark 1.1 1 --json
taocp benchmark 1.1 1 --reuse

Benchmark cost is split into fast generation, the complete slow workflow, and blind quality evaluation. The evaluation calls are not added to either mode's production cost. Each run saves fast, slow, and report.json artifacts under the configured output directory.

Run the reproducible five-exercise model matrix:

taocp matrix --write-manifest matrix.json
taocp matrix --manifest matrix.json --parallel 2 --resume

The built-in manifest covers five difficulty levels, five limited-time Zen routes, twelve local GamingPC models, and six GPT models. It runs every profile in fast mode and adds a matched slow-mode run for GPT-5.6 Sol. One fixed GPT-5.6 Sol evaluator builds a single reference per exercise, then applies a reference-grounded criteria judge and a reference-blind falsification judge to every solution. Provider failures and evaluation failures are separate from false solutions. The resumable report preserves each solution, both audits, every token component, published price card, generation cost, evaluation cost, latency, and aggregate capability rates. See the matrix protocol and the 2026-07-20 Zen evaluation.

Flags can appear before or after positional arguments. Every model-calling command accepts --base-url, --api-key, --model, --source, --output, --timeout, and --retries.

Library

The root package is named taocp. Public subpackages expose the transport, benchmark runner, configuration, exercise loader, prompts, pricing, result store, solver engine, and text guards.

package main

import (
	"context"
	"log"

	taocp "github.com/tamnd/taocp-solver"
	"github.com/tamnd/taocp-solver/solver"
)

func main() {
	cfg := taocp.DefaultConfig("http://localhost:8790/v1", "")
	client, err := taocp.New(cfg)
	if err != nil {
		log.Fatal(err)
	}

	answer, err := client.SolveReference(context.Background(), "1.1.1", solver.Options{
		Mode:           solver.ModeSlow,
		MaxCorrections: 2,
	})
	if err != nil {
		log.Fatal(err)
	}
	log.Printf("true: %t, tokens: %d, list cost: $%.6f",
		answer.Evaluation.True,
		answer.Metrics.CurrentRun.Tokens.TotalTokens,
		answer.Metrics.CurrentRun.ListCost.TotalUSD)
}

Use taocp.WithCompleter to supply a custom model transport, taocp.WithRepository for a custom content source, and taocp.WithStore for a custom output location.

Configuration

Environment variable	Default	Purpose
TAOCP_SOLVER_BASE_URL	none	Bridge or proxy base URL
TAOCP_SOLVER_API_KEY	OPENAI_API_KEY	Endpoint credential
TAOCP_SOLVER_MODEL	gpt-5.6	Model name
TAOCP_SOLVER_SOURCE	~/github/tamnd/taocp	TAOCP content repository
TAOCP_SOLVER_OUTPUT	~/data/taocp-solver	JSON and Markdown results
TAOCP_SOLVER_TIMEOUT	30m	Timeout for each model call
TAOCP_SOLVER_MAX_CORRECTIONS	2	Correction passes
TAOCP_SOLVER_CANDIDATES	3	Independent solution candidates, from 1 to 5
TAOCP_SOLVER_MAX_RETRIES	4	Transient transport retries
TAOCP_SOLVER_PARALLEL	2 or available CPUs	Batch workers

The output store writes {section}/{number}.json and {section}/{number}.md atomically. JSON keeps the final solution, both latest judge reports, truth decision, model response identifiers, token counts, list-cost estimates, timestamps, and the complete attempt sequence.

Metrics and list cost

Every model call records input, cached-input, cache-write, output, reasoning, and total tokens. Output tokens already include reasoning tokens, so reasoning is reported as a detail and is never charged twice. Result metrics have two scopes:

• current_run counts only requests made by the current command.
• cumulative counts the saved solution attempt history, including an earlier solve when a cached solution is reviewed again.

Each scope includes a complete provider-reported token breakdown, priced and unpriced request counts, and a standard API list-cost estimate in USD. GPT-5.6 Sol, Terra, Luna, GPT-5.5, GPT-5.4, and GPT-5.4 mini rates come from the official model documentation. The calculator includes the official 1.25x cache-write rate when the endpoint reports cache-write tokens, plus applicable input and output multipliers for requests above 272K input tokens. GPT-5.4 mini does not use that long-context multiplier.

The matrix also records each free route's published list price. OpenCode Zen explicitly lists DeepSeek V4 Flash Free, MiMo-V2.5 Free, North Mini Code Free, and Nemotron 3 Ultra Free at zero for input, cached input, and output. Zen does not publish a cache-write price for them. Hy3 is recorded from Tencent Cloud's upstream price card: free through July 22, 2026, then CNY 1 input, CNY 0.25 cache hit, and CNY 4 output per million tokens. Zen does not publish hy3-free in its own pricing table, so the report does not present Tencent's price as a Zen price. Local models remain unpriced because a zero API charge does not measure electricity or hardware depreciation.

List cost does not claim actual subscription cost, or Batch, Priority, tool-call, negotiated, hardware, or energy cost. An unknown price is reported as unavailable instead of being assigned an invented zero.

Development

make fmt
make vet
make test
make lint

Tests use local HTTP servers and scripted model responses. They do not require credentials or network access.

Evaluation references

• AdvancedMathBench reports low true-negative rates for frontier proof verifiers and evaluates both correctness verdicts and fine-grained proof-error rationales.
• MaxProof combines proof generation, verification, critique-conditioned repair, population-level test-time scaling, and tournament selection.
• Scaling Generative Verifiers finds that combining generative selection and judge-based verification outperforms either approach alone, while warning that procedural quality can diverge from mathematical validity.
• MA-ProofBench demonstrates a large gap between natural-language judgments and formal proof acceptance, with incomplete proofs among the dominant failure modes.
• ProofGrader and ProofBench study rich reference context, problem-specific marking schemes, fine-grained proof scoring, and evaluator ensembles.
• ProcessBench evaluates critics by whether they find the earliest incorrect reasoning step.
• Math-Verify separates answer extraction, normalization, and mathematical equivalence checks.
• PRM800K provides step-level correctness supervision and conservative symbolic answer grading.

License

MIT