When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization

arXiv:2611.07073v1 Announce Type: new Abstract: A verified Dafny postcondition certifies that a formula holds, but it does not guarantee that the result was reached through genuine independent reasoning. We introduce a cross-agent formalization protocol where a Specifier model translates clinical trial criteria into a Dafny predicate, and an Implementer model writes an operational method checked against it. A same-model control establishes that even with no capability gap, independent re-extraction from identical text agrees only 59.3% of the time. Evaluating four model configurations on 96 clinical trial documents, we find that agreement is highly sensitive to how model capability is allocated across the two roles: the GPT-4.1-nano/GPT-4.1-mini configuration achieves 53.0% agreement when the stronger model is the Implementer, but only 14.3% when the roles are reversed. The strongest tested configuration, GPT-5.6-luna/GPT-5.4-mini, improves agreement to 34.4% but remains below the same-model baseline and is dominated by direct contradiction (42.7%). We also detect a critical verification artifact in which a weaker Implementer satisfies the postcondition by invoking the Specifier's predicate directly; after structural auditing, corrected agreement falls from 14.3% to 13.2%. Our results show that verification success alone is insufficient evidence of independent cross-agent agreement, and that model capability does not guarantee agreement when formalizing the same source independently.

Verification success does not guarantee independent cross-agent agreement, highlighting limitations of AI models.

SOURCE     arXiv cs.AI (tier 1)
   ↓
DOCUMENT   53806361-b5e3-4859-9bd4-8bb9f7d90c89
           https://arxiv.org/abs/2611.07073
   ↓
EVIDENCE   3 extracted excerpts
   ↓
MODEL RUN  1 run, methodology 1.0.1
   ↓
SCORE      -50  (Adverse)
   ↓
CONFIDENCE 80%