coconut

Differential comparison of LLM-generated formal specifications.

Motivation

Autoformalization has a trust problem: when an LLM translates a natural-language problem statement into a formal specification, there is no ground truth to check the spec against. This project explores a way to get a correctness signal without ground truth — differential specification:

1. Give the same natural-language problem to several independent frontier LLMs.
2. Have each one emit a formal spec of the problem's answer function.
3. Compare the specs to each other with a solver and classify each pair as equivalent, one-stronger, incomparable, or unknown.

Unanimous agreement across independent models is evidence that the problem statement is unambiguous and the formalization faithful; disagreement pinpoints either an ambiguous problem or a model's misreading. This is useful both as a benchmark of LLM formalization ability and as a quality filter for datasets like FVAPPS (formally verified APPS), which supplies the problems here (data/fvapps.jsonl, ~4,700 competitive-programming problems).

Two designs: diffspec (abandoned) → spec_gen (current)

v1 — diffspec (Dafny). The original plan had models emit free-form Dafny specs, which would be structurally parsed (parser.py) and then compared (compare.py) by generating implication lemmas, shelling out to the Dafny verifier/Z3, and falling back to adversarial random sampling when Z3 returned UNKNOWN. The full designs survive as parser_spec.md and compare_spec.md (both very detailed and still worth reading for the verdict semantics: EQUIVALENT / A_STRONGER / B_STRONGER / INCOMPARABLE / UNKNOWN). This path was abandoned — free-form Dafny needs a parser, a Dafny→Python translator, and subprocess orchestration, and still can't guarantee a verdict. The source was removed (git log: "Remove diffspec/compare.py"); test/diffspec/test_parser.py and smoke.dfy are leftovers with no corresponding source.

v2 — spec_gen (JSON AST + Z3, current). Instead of free-form Dafny, the system prompt (the "K1 contract" in src/spec_gen/prompts.py) forces every model to emit its spec as a JSON AST in a deliberately tiny fragment:

• scalar Int/Bool arguments only, positionally named a0, a1, … so specs from different models line up;
• linear integer arithmetic only — multiplication/division/modulo by constant only, no quantifiers, no collections, no recursion;
• optional assumes (preconditions) plus a single body expression.

That fragment is quantifier-free linear integer arithmetic, which Z3 decides completely — so pairwise spec comparison can always return a definitive verdict, no fallback engine required. Expressiveness is traded for decidability.

Pipeline

FVAPPS problem (NL)                          data/fvapps.jsonl
        │
        ▼
ast_generator.py    fan out to 5 models via OpenRouter (models.yaml):
                    Claude Sonnet 4.6, GPT-5.5, Gemini 3.5 Flash,
                    Grok 4.3, DeepSeek v4 → one JSON AST spec each
        │
        ▼
format_verification.py   deterministic (no model in the loop) check that a
                         spec obeys the K1 contract; reports every violation
        │
        ▼
converter.py        lower a valid AST into Z3 expressions
        │
        ▼
[NOT YET BUILT]     pairwise Z3 equivalence check → verdict per model pair

Repository layout

src/spec_gen/
  prompts.py               SYSTEM_PROMPT_K1 — the JSON-AST spec contract
  ast_generator.py         load FVAPPS problem, fan out to models, strip fences
  format_verification.py   deterministic K1-contract validator
  converter.py             AST node → Z3 expression (build_vars + conv)
data/
  fvapps.jsonl             FVAPPS problems (apps_id, apps_question, …)
  output/                  generated records: {apps_id, {model: spec_json}}
test/
  spec_gen/
    smoke_test.py               live end-to-end run (spends tokens; manual)
    test_format_verification.py unit tests for the validator
  diffspec/
    test_parser.py         orphaned — tests for the removed v1 parser
models.yaml                OpenRouter model roster + defaults
parser_spec.md             v1 design doc (Dafny parser) — historical
compare_spec.md            v1 design doc (Dafny comparator) — historical
smoke.dfy                  v1 leftover fixture

Running

uv sync
cp .env.example .env       # set OPENROUTER_API_KEY

# generate specs for one problem across all models (live API calls)
uv run python test/spec_gen/smoke_test.py 0042

# unit tests (no network)
uv run pytest test/spec_gen/test_format_verification.py

Where I left off

Generation, format verification, and AST→Z3 lowering work; the actual comparison — the point of the project — is the missing piece.

Done:

• Multi-model spec generation runs end to end (data/output/0001.json and 0514.json are real five-model records).
• format_verification.py validates specs against the K1 contract with tests.
• converter.py converts every allowed AST node to Z3 (last commit: "Add spec_gen AST->z3 converter").

Next steps, roughly in order:

1. Finish converter.py's top level. build_vars and conv exist, but there is no function that assembles a whole spec (signature + assumes + body) into a Z3 formula, and conv is untested.
2. Write the pairwise comparator. For two specs over the same signature, ask Z3 whether assumes_A ∧ assumes_B ⟹ body_A = body_B (and the directional variants), reusing the v1 verdict vocabulary (EQUIVALENT / A_STRONGER / B_STRONGER / INCOMPARABLE). Decide how to handle mismatched signatures/assumes between models — that mismatch is itself a disagreement signal worth recording.
3. Wire format verification into the generation loop — ast_generator currently stores whatever the model returns without running the validator.
4. Batch runner + results. Sweep FVAPPS, store verdict matrices per problem, and aggregate agreement statistics per model pair.
5. Housekeeping. data/ and test/diffspec/ are untracked; commit the outputs (or gitignore them) and delete or archive the orphaned diffspec tests, smoke.dfy, and placeholder main.py.