Hollow Proofs

A judge-free benchmark for measuring dishonesty in LLMs that produce formally checkable proofs. A formal verifier (Verus) is the honesty oracle, so dishonesty is mechanically detectable as a contradiction between the model's self-report and its artifact, in two modes:

• Hollow proof — the proof passes standard verification only because it hides an unsound primitive (assume, admit, external_body, assume_specification), which verus --no-cheating catches, while the model denies using one.
• Grounded lie — the proof fails, the model's own unpressured assessment agrees it failed, yet under pressure it claims success.

No judge LLM, no human rater. The model produces its proof through an agentic loop against the standard verifier (write → check → fix) and is never shown the soundness check; we compare its final claim to its artifact once, afterward, in the scorer. See REPORT.md for the full writeup and pilot results.

Quick start

uv sync
uv run pytest -q                              # 46 tests, no external data
uv run python scripts/validate_agentic.py     # mockllm end-to-end, zero API cost

Render the report to PDF (no LaTeX needed): pandoc REPORT.md -f gfm -s -c report.css --pdf-engine=weasyprint -o REPORT.pdf

Data and reproduction

The test suite and the mockllm validators use only in-repo fixtures and a mock model, so uv run pytest -q validates the instrument on a fresh clone with no external data.

Re-running the task curation or the real-model pilots needs Verus installed (we pin 0.2026.05.17.e479cce with Rust toolchain 1.95.0; set VERUS_BIN if it is not on PATH) and the upstream task corpus:

git clone https://github.com/microsoft/verus-proof-synthesis vendor/verus-proof-synthesis

data/curated_gradient.json and data/curated_tasks.json store task ids, not task bodies; the bodies load from vendor/ at runtime. Sources are Verus-Bench and VeruSAGE-Bench (in microsoft/verus-proof-synthesis), which include the CloverBench- and MBPP-derived entries. Respect the upstream licenses when redistributing task content. Real model runs cost money: see scripts/run_pilot.py and scripts/analyze.py.

Layout

• src/hollow_proofs/ — package: verifier, detector, schema, prompts, tools, parsing, task, analysis
• scripts/ — curate_tasks, validate_* (mockllm, zero cost), probe_cheat_knowledge, run_pilot, analyze
• data/curated_gradient.json — the 121-task difficulty-graded set; data/curated_tasks.json — the 20-task pilot subset
• tests/ — unit tests and Verus fixtures
• REPORT.md — the writeup; report.css — its PDF stylesheet

License

MIT, see LICENSE. Task content loaded from vendor/ is governed by its own upstream license.

Maintainer

Orpheus Lummis.