fm-loop-engineering

name

fm-loop-engineering

description

Use when running or extending the fmhub formal-verification benchmarks — driving LLMs (codex / DeepSeek V4 Flash & Pro / GLM) to add ACSL/Dafny/Verus specs that a verifier proves, and lifting weaker/cheaper models toward codex quality via loop engineering. Covers the harness toolkit, the proven workflow levers, the Flash+Pro cascade, model/endpoint gotchas, and how to add a solver. Trigger on tasks about FMBench, spec generation, multi-turn verifier loops, hybrid model cascades, or improving a weak model's pass rate on these benchmarks.

FM Loop Engineering Playbook

Thesis: codex's strength is half MODEL, half WORKFLOW. The workflow is a transferable lever — borrow codex's loop patterns to lift cheap models (DeepSeek Flash/Pro) toward codex quality at a fraction of the cost. See LOOP_ENGINEERING_THESIS.md and BENCHMARK_METHODOLOGY.md.

The harness toolkit (benchmarks/)

harness	when to use	key file
linear multi-turn	default; low-cheat models (DeepSeek)	run_fmbench_multi.py
hybrid Flash→Pro cascade	cost-optimal; the main deliverable	run_fmbench_hybrid.py
insertion-only (cheat-proof)	egregious cheaters (GLM 85%)	run_fmbench_insert.py
source-locked (reject cheats)	cheat detection studies	run_fmbench_locked.py
GDR scaffold / agent	width/agency experiments	run_fmbench_gdr.py / run_fmbench_agent.py

The proven levers (apply in this order)

1. Multi-turn verifier feedback — biggest lever (DeepSeek 31%→57%). Feed WP's proved/total + failing goals back each round.
2. parse_error mitigation (acsl_syntax.py) — categorize + targeted repair + mechanical_fix() before verify. Drops parse_error ~13→2 on hard tasks.
3. Persistence prompt — inject codex's "keep going until WP proves every goal, persevere through failures, don't guess." DeepSeek gives up too early.
4. Flash→Pro cascade — Flash (cheap) solves the easy ones; escalate residual to Pro. Route on WP signal. Most passes land on cheap Flash.
5. agent + run_eva — for hard proof gaps, let the model self-discover invariant bounds via EVA. 6. pass@N — exploit weak-model variance (cheap on Flash).

Borrowed from codex (open source: openai/codex, cloned analysis)

• apply_patch context-anchored edit format (codex-rs/apply-patch) — anchor edits to verbatim lines, not line numbers; +/- prefixes keep ACSL backslashes literal (NO JSON — \forall/\result get corrupted by JSON escaping).
• Persistence prompt (codex-rs/core/gpt_5_2_prompt.md).
• Verify-in-loop + update_plan tracking.

Critical gotchas

• Faithfulness is mandatory: a WP pass means nothing if the model deleted the asserts. Always check_faithfulness. GLM's 100% WP was 85% cheating.
• Insertion harness hurts non-cheaters: it breaks loop-invariant placement → parse_error. Use linear for DeepSeek; insertion only for GLM-class cheaters.
• Endpoint matters: GLM coding-plan = 80% empty content; OpenRouter = 0%. Set high max_tokens (24000) for reasoning models. See BENCHMARK_METHODOLOGY.md §2.
• Anti-hang: always route LLM calls through llm_robust.robust_chat (hard 300s deadline). Naive retry hung GLM 34 min.
• Solver dispatch: SOLVER={codex|deepseek|glm|openrouter} monkey-patches the chat adapter at import. A standalone runner MUST import solver_dispatch BEFORE importing codex_adapter_chat, or it won't switch.

Adding a model / endpoint

1. Make a <name>_adapter.py + <name>_adapter_chat.py that delegate to llm_robust.robust_chat(client, model, history, RETRYABLE, max_tokens=...).
2. Add a branch to solver_dispatch.py.
3. Reasoning models: high max_tokens + empty-content retry (see glm_adapter_chat).
4. Run: SOLVER=<name> <KEY>=... python3 bench_parallel.py fmbench_multi -K 5 -w 8 ...

Cost-optimal default

run_fmbench_hybrid.py (Flash→Pro + acsl_syntax + persistence) is the recommended production path: codex-class results trajectory at mostly-Flash cost. Verify on the 20 hardest tasks (/tmp/glm_locked_sample.json) before scaling.