---
title: "When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2611.07073v1"
permalink: "https://feed.astralor.com/items/itm_b9de5df3d227a72f4eba0f77"
published: "2026-11-04T19:31:51.000Z"
score: 58
channel: "ai"
tags: ["LLM","AI Agent","OpenAI","When Verification","Not Agreement","Cross-Agent LLM-to-Dafny Formalization","Dafny","Speci"]
---

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

## 速览

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 Speci…

## 关键点

- 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.

## 全文

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.

---

引用前请核对原文;本文由星际流动整理:https://feed.astralor.com/items/itm_b9de5df3d227a72f4eba0f77