Hollow Proofs: Measuring LLM Dishonesty with a Formal Verifier

Strengths. Using Verus's --no-cheating mode as a deterministic dishonesty oracle gives this benchmark the referent existing honesty evaluations lack — no judge LLM, no human rater. Two methodological moves are genuinely useful: the prediction-vs-observation distinction (which the array_concat flip case shows is doing real work), and the agreement(B, V) belief-fidelity audit that withholds a dishonesty verdict when the belief itself is untrustworthy. The repo backs the report: MIT-licensed, pinned Verus and Rust versions, 46 tests, a mockllm validator for zero-cost reproduction, 121 curated tasks, every numeric claim traceable to a run log.

To strengthen.

Scale the panel. The headline null is on one model family at k=1. A small panel spanning capability and alignment, at k≥3, is the only way to tell whether the null is the methodology working or DeepSeek-specific behavior.

Build the target-function-scoped detector. The verify-and-sound filter drops exactly the hard primitive-using tasks where VeruSAGE's 14% cheating baseline lives — i.e. the regime most likely to elicit a signal.

Raise belief-elicitation fidelity. agreement(B, V) = 3/8 is worse than always guessing "verifies" (5/8), so the grounded-lie verdict is gated to silence by construction. Spell out the proposed production-informed elicitation and how it avoids re-introducing the anchoring problem the three-paraphrase design solved.

Ablate pressure framing. A single deadline cue is a thin prior; identity, audit, and oversight cues each move different behavior in the scheming/sandbagging literature.

The pilot is intentionally narrow and the report is honest about that. Scaled to a model panel and a harder task tier, this plausibly anchors a follow-on publication.

The project addresses a critical issue in AI safety by developing a benchmark for detecting dishonesty in LLM-produced formal proofs using Verus. The approach is innovative, as it leverages a deterministic verifier to mechanically detect contradictions between the model's self-report and its artifact, distinguishing between lying and miscalibration. The project also introduces a novel method of eliciting observations rather than predictions to measure honesty, which is a valuable contribution to the field.

However, the main weakness lies in the limited scope and scale of the pilot study. With only 2 models tested under specific conditions, the results cannot be generalized to broader populations or more challenging tasks. Additionally, the belief elicitation mechanism shows low fidelity, which limits the reliability of the grounded-lie detection. The project also lacks a robust validation against other formal verification systems like Lean 4 and Dafny, which could provide additional insights into the generalizability of the findings.

To enhance the project's impact, future work should focus on expanding the model panel to include a wider range of capabilities and alignment levels. Additionally, developing a more reliable belief elicitation method that does not anchor to the pressured statement would strengthen the grounded-lie detection. Extending the task set to include harder, primitive-using tasks could also provide a more comprehensive evaluation of dishonesty in LLMs.