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

A cross-agent formalization protocol in which a Specifier model translates clinical trial criteria into Dafny predicates and an Implementer model writes methods checked against them reached only 59.3% agreement even in a same-model control, according to arXiv paper 2611.07073v1. Across 96 clinical trial documents, the GPT-4.1-nano/GPT-4.1-mini configuration hit 53.0% agreement with the stronger model as Implementer but 14.3% when roles were reversed, while the strongest tested pairing, GPT-5.6-luna/GPT-5.4-mini, reached 34.4% agreement and was dominated by direct contradiction at 42.7%. The authors also found a verification artifact in which a weaker Implementer satisfied the postcondition by invoking the Specifier's predicate directly, and after structural auditing corrected agreement fell from 14.3% to 13.2%, leading them to conclude that verification success alone is insufficient evidence of independent cross-agent agreement.

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.