Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 24, 2026Sofia, Bulgaria

Cross-Model Spec Comparison: Finding Disagreement in Candidate Lean 4 Specifications Generated by OpenAI Models

Henry Ward

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: Cross-Model Spec Comparison: Finding Disagreement in Candidate Lean 4 Specifications Generated by OpenAI Models

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

We study whether candidate formal specifications produced by different OpenAI models agree on the intended behavior of small systems. For three specification tasks, we generate three Lean 4-oriented candidates per task, normalize them into a shared canonical format, and compare assumptions, preconditions, postconditions, invariants, and semantic boundary choices. We then search for concrete counterexamples using executable validators and property-based style witnesses. In the live OpenAI-backed run, the models converged on the sortedness and token-bucket tasks, but diverged sharply on token expiry: every pairwise comparison for that task produced a counterexample at the exact expiry boundary. The main takeaway is that cross-model disagreement is a practical signal for underspecification when the prompt exposes a crisp semantic boundary, and that a lightweight normalization plus witness-generation pipeline can turn that disagreement into reportable evidence under a very small budget.

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. A clean, honest proof of concept, and the token-expiry result is the most convincing of the three: every model pair splits at exactly the inclusive/exclusive boundary, the kind of ambiguity that can undermine a specification. The disposition is right throughout: the two converging tasks are reported as such, and the dual-use risk is raised without prompting. The evidence is thinner than the claim, though. One of three tasks produced any disagreement at all, and its witness was hand-seeded for precisely the boundary it found, so the result partly shows that a check finds the case it was written to find. That also leaves the two 0/9 convergences uninterpretable: a settled spec, or a prompt that was simply not adversarial enough? A benchmark of boundaries that were not pre-seeded, together with a measured false-positive rate for the disagreement classifier the authors themselves call noisy, is what would carry this from a demonstration to a method.

    Read full reviewShow less

  2. Good work. This is a cool project that is filled with good ideas, albeit its evaluation scope is fairly small.

Cite this project

@misc{ward2026crossmodel,
  title = {{Cross-Model Spec Comparison: Finding Disagreement in Candidate Lean 4 Specifications Generated by OpenAI Models}},
  author = {Henry Ward},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/crossmodel-spec-comparison-finding-disagreement-in-candidate-lean-4-specifications-generated-by-openai-models-dqnh}},
  url = {https://apartresearch.com/sprints/projects/crossmodel-spec-comparison-finding-disagreement-in-candidate-lean-4-specifications-generated-by-openai-models-dqnh}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026