Source-linked AI summary
Beyond Correctness: Attribution of Natural-Language Documentation for Formal Libraries
Sirui Jiang, Dongming Xiang, Shichao Wu, Yuxuan Zhou, Yihong Wu, Fangze Zhu, Wang Lin, Guanjun Liu
TL;DR
True documentation can still say nothing about a function's specific behavior. DocAuth checks whether statements distinguish the target from interface-conforming alternatives and publishes them with formal properties and evidence. In the evaluation, DocAuth increased the share of published sentences confirmed attributable from 82.9% under truth-only checking to 94.7%.
Problem
A documentation statement can be true yet restate only an interface fact or general fact, rather than describe the function’s specific behavior.
Source: §1 · p. 2Method
DocAuth checks whether a statement fails for an alternative implementation satisfying the same interface, then publishes sentences with their recovered formal properties and evidence.
Source: §1 · pp. 2, 4Results
94.7% of published sentences were confirmed attributable with DocAuth versus 82.9% under truth-only checking; DocAuth delivered 37% more attributable sentences than mutation filtering.
Source: §1 · p. 4Takeaways & Limitations
Attribution complements truth by checking whether documentation describes behavior beyond what callers can learn from the interface.
Source: §1 · p. 2The evaluation covers stateless ACL2 Community Books functions with extractable definitions and three LLMs, each run once at temperature 0.
Source: §6 · p. 17
Abstract
from arXiv · showhide
Formal languages are widely used in software engineering to specify and verify program properties. Because their mathematical notation and logic are hard to read, developers often rely on natural-language documentation to understand the functions in formal libraries. Yet a documentation statement can be provably true and still hold after the function's behavior changes. We call a statement's dependence on the function's specific behavior attribution, and we give a method to check it. We design and implement DocAuth, a documentation-generation method that uses attribution to decide what to publish and attaches to each published sentence the formal property recovered from it, together with checkable evidence. On 150 functions from the Community Books library of the ACL2 theorem prover, three large language models produce proved but non-attributable properties for about a third of the functions. DocAuth matches or exceeds the attribution rate of a mutation-based filter while delivering 37% more attributable sentences. Compared with a pipeline that checks truth alone, it raises the share of published sentences that a second model confirms as attributable from 82.9% to 94.7%. These results show that provable truth does not guarantee that documentation reflects what a function actually does. Attribution complements truth as a criterion for generating and evaluating documentation for formal libraries.
1 Introduction
Natural-language documentation helps readers navigate formal libraries, but a proved statement may still reveal nothing about a function’s behavior. The paper defines attribution relative to the public interface, builds DocAuth to check it, and evaluates the method against truth-only and mutation-based filtering.
1 Introduction
- Formal notation and jointly informative theorems can be difficult to read, while generated documentation is commonly checked for provability or code consistency.Examples include an ACL2 statement that reduces to a return-type fact and a Lean statement that follows from equality substitution; both are true but implementation-independent.Source: §1 · pp. 1–2
- Attribution holds when a target-valid statement fails for at least one alternative implementation satisfying the same public interface.An interface-conforming witness and a failing input make the verdict checkable; non-attribution is established by a proof covering all conforming implementations.Source: §1 · pp. 2–3
- Attribution evaluates whether an individual statement adds behavioral information beyond the interface, a question existing measures do not answer.Mutation methods may change too little or fail to preserve the interface, while vacuity and semantic-dependence checks may change too much; the comparison is summarized in Table 1.Source: §1 · pp. 2–3, Table 1 · p. 3
- DocAuth checks candidate properties, renders retained properties as sentences, recovers a formal property from each sentence, and publishes only sentences whose recovered property passes attribution.Each published sentence is accompanied by its recovered property and evidence.Source: §1 · pp. 3–4
- On 150 ACL2 Community Books functions, DocAuth raises attribution confirmation from 82.9% to 94.7% versus truth-only checking and yields 37% more attributable sentences than mutation filtering.Pooled over three generator models, DocAuth also delivers the most attributable sentences at the highest attribution rate among the compared methods.Source: §1 · pp. 3–4
2 Attribution
Attribution distinguishes properties tied to a function’s behavior from those that hold for every implementation allowed by its interface. The checking method combines erasure proofs with interface-conforming witnesses, while finite searches that find no witness remain inconclusive.
2 Attribution
- For base64-encode-list, the return-type property holds for any character-list-returning implementation, but the property that encoding nil returns nil fails for an alternative implementation.ACL2 proves both properties; an implementation that always returns a one-character list preserves the first and falsifies the second.Source: §2 · p. 4
2.1 Formal Definition
- A target-valid property is attributable when some same-interface implementation and input falsify it; it is non-attributable when no such witness exists.The definition also distinguishes confirming a witness within a finite search from proving that no witness exists at all.Source: §2.1 · p. 4
- A target proof plus one witness confirms attribution, but a finite search that finds no witness cannot establish non-attribution.The checker searches finite sets of alternative implementations and input assignments generated by fixed rules.Source: §2.1 · p. 4
2.2 Checking Method
- The erased environment replaces the target with a fresh symbol constrained by its return contract, enabling a proof there to establish non-attribution under the stated dependency condition.Inputs remain constrained by the interface, and properties depending on other functions that call the target are left unresolved.Source: §2.2 · p. 5
- The checker classifies completed properties as attributable, non-attributable, or no-witness-found; unavailable dependencies, incomplete checks, and unsatisfied premises yield unresolved outcomes.The original environment checks properties not proved in the erased environment; counterexamples there mark a property false for the target.Source: §2.2 · p. 5
3 DocAuth
DocAuth selects attributable formal properties, renders them as sentences, and rechecks the properties recovered from those sentences before publication. It supplies published sentences with their recovered properties and checkable attribution evidence.
3 DocAuth
- DocAuth publishes a sentence only after checking both its candidate property and the property recovered from the rendered sentence for attribution.The recheck matters because rendering can change a property's meaning or scope; published sentences include the recovered property and its evidence.Source: §3 · pp. 5–6, §3.3 · p. 8
3.1 Candidate Generation
- Candidate generation uses the function body to propose behavior worth documenting, while leaving attribution filtering to later checks.The prompt requests result shape, input relationships, boundary cases, and behavior under composition with standard functions, but does not mention attribution or erasure.Source: §3.1 · pp. 6–7
3.2 Implementing the Check
- The check proves non-attribution in an erased environment, then searches interface-valid alternatives and inputs for a witness that falsifies the property.Alternative templates are admitted only when ACL2 proves they satisfy the interface; unresolved searches or searches without a witness do not support publication.Source: §3.2 · pp. 7–8
3.3 Rendering and Rechecking
- A separate model back-translates each rendered sentence without seeing the original candidate property, and DocAuth checks the recovered property before publishing.For example, a sentence that only says the encoded result is a character list is rejected because that property merely restates the return type.Source: §3.3 · p. 8
4 Evaluation
Across the ACL2 evaluation, generated properties were often true but non-attributable, while DocAuth improved the attribution and yield of published sentences. The results also show how parameter settings, unresolved checks, and runtime constrain its coverage and cost.
4.1 Experimental Setup
- The evaluation uses 150 pseudo-randomly selected ACL2 functions, three generator models, and a cross-model reassessment of published sentences.The target pool was selected from 162 eligible functions among 2,054 functions; models generated 15 properties per function, and the sentence experiment allowed at most four sentences per function.Source: §4.1 · pp. 8–9
4.2 RQ1 (Prevalence): How Common Are Non-Attributable Properties?
- 35.0%, 32.3%, and 29.9% of functions with completed checks have at least one non-attributable property from Qwen2.5-7B, DeepSeek-v4-flash, and GPT-5.6-terra, respectively.From Qwen2.5-7B to GPT-5.6-terra, false-for-target properties fall from 39.7% to 2.0%, while non-attributable properties fall from 8.5% to 5.3%; 87.8% of library-authored theorems are attributable.Source: §4.2 · pp. 9–10, Table 2 · p. 9
4.3 RQ2 (Criterion Validity): Do Attributable Properties Detect Interface-Preserving Implementation Changes?
- Most attributable properties (64.8%) detect interface-preserving implementation changes that played no role in their check, versus 15.3% of target-holding properties with no witness and 0/48 non-attributable properties.Pooled across four groups, 614 of 948 attributable properties detect at least one change; among 507 property–change failures in GPT-5.6-terra’s proved properties, 503 (99.2%) involve attributable properties.Source: §4.3 · p. 10
4.4 RQ3 (Method Effectiveness): Does DocAuth Improve the Attribution of Generated Documentation?
- 94.7% of published sentences are confirmed attributable with DocAuth, versus 82.9% with truth checking; DocAuth delivers 319 more attributable sentences than mutation filtering.DocAuth’s attribution rate is 2.7 points above mutation filtering’s 92.0%; the sentence recheck raises rates, while selecting attributable candidates increases yield.Source: Figure 6 · p. 11, §4.4 · pp. 11–12, Table 4 · p. 12
4.5 RQ4 (Parameter Effects): How Do Budget Settings Affect the Yield of Attributable Content?
- Larger candidate budgets and witness-search scopes yield more attributable content with diminishing returns, while publishing more sentences per function barely lowers attribution rates.For GPT-5.6-terra, increasing k from 3 to 15 raises attributable properties from 311 to 1,209 but lowers their share from 73.9% to 57.8%; after the 16th alternative, 63 properties remain without a witness. Increasing m from 1 to 4 raises attributable sentences from 354 to 1,172 while the rate falls from 96.7% to 94.7%.Source: Figure 7 · p. 14, §4.5 · p. 14
4.6 RQ5 (Coverage and Cost): How Many Functions Are Covered, and at What Cost?
- 70.0%–84.7% of functions are covered, and an end-to-end run takes a median of 219.8 seconds per function and costs about $0.048 in model calls.Unresolved outcomes account for 34.4%–56.4% of checked properties, far more than the 1.4%–3.6% with no witness found; generated-property unresolved outcomes mainly reflect missing target proofs or evaluation failures.Source: §4.6 · pp. 14–16, Figure 8 · p. 15, Table 6 · p. 15
5 Discussion
The discussion argues that attribution adds a behavior-specific criterion to documentation evaluation, alongside correctness. Its checkable evidence supports comparison under a shared interface, while broader quality measures and studies remain future work.
5 Discussion
- Attribution complements correctness by testing whether a true behavior statement also fails for an implementation satisfying the same interface.The authors suggest reporting attribution rates alongside correctness measures; every verdict comes with checkable evidence.Source: §5 · p. 16
- Attribution rates should be compared under the same interface, because a stronger interface leaves fewer statements attributable.The measure can also assess existing documentation, with prover-oriented lemmas set aside first when using library theorems.Source: §5 · p. 16
- Future work includes mainstream-language documentation, combining attribution with other quality measures, developer studies, and testing real code evolution.The authors note that executable alternatives may provide witnesses in mainstream languages, while proving truth and non-attribution still requires a verifier.Source: §5 · p. 16
6 Threats to Validity
The evaluation has limits in construct validity, measurement, and experimental scope. It does not establish whether attributable documentation benefits developers, and sentence-meaning recovery remains unvalidated by human judgment.
6 Threats to Validity
- No developer study tested whether attributable documentation helps developers understand or maintain code, or how much effort attached evidence takes to inspect.Attribution measures behavior beyond the interface, while usefulness also depends on importance, completeness, and readability.Source: §6 · p. 17
- Meaning recovery uses an LLM and the same checker as publication; interface-only reassessment and RQ3 reduce code-reliance risk but do not replace human judgment.Source: §6 · p. 17
- Experiments cover stateless ACL2 Community Books functions with extractable definitions and three LLMs run once at temperature 0.Other prompts, sampling settings, or model versions may yield different properties; stateful, interactive, or concurrent programs pose different modeling demands, and other provers need their own interface extraction and erasure environment.Source: §6 · p. 17
7 Related Work
Related work tests specifications through code changes, documentation through correctness or consistency, and properties through redundancy pruning. The paper distinguishes attribution by checking each true statement against the public interface.
7 Related Work
- Unlike specification-testing methods, attribution examines already-true individual statements against the public interface and proves non-attribution by erasure rather than relying on a missing distinguishing implementation.The compared methods include nl2postcond [Endres et al. 2024], MutDafny [Amaral et al. 2026], and IronSpec.Source: §7 · p. 17
- Documentation evaluations use textual similarity, correctness, consistency, or tests, while attribution detects true statements that only restate an interface or general fact.The passage contrasts attribution with source support, whole-document behavioral equivalence, and regenerating summaries after code changes [Rashkin et al. 2023; Eghbali et al. 2026; Zeng et al. 2026; Khatib et al. 2026].Source: §7 · pp. 17–18
- Property-generation tools prune results implied by other properties or lemmas, whereas attribution asks whether each true statement adds behavior beyond the published interface.Attribution confirms with a witness and establishes non-attribution with an erasure proof; DocAuth also rechecks recovered properties, linking it to autoformalization [Cosler et al. 2023; Wu et al. 2022].Source: §7 · p. 18
8 Conclusion
The conclusion argues that truth alone cannot ensure documentation describes a function’s specific behavior. Attribution offers a complementary check for documentation generation and evaluation.
8 Conclusion
- Attribution distinguishes true statements that add behavior beyond the interface, and DocAuth publishes attributable sentences with recovered formal properties and evidence.The evaluation found non-attributable properties in about a third of studied functions; DocAuth delivered more attributable sentences than truth checking and mutation filtering, at a higher attribution rate.Source: §8 · p. 18
9 Data Availability
The replication package is planned for permanent archiving and will include materials for offline recomputation and execution-context details.
9 Data Availability
- The planned permanent archive includes source snapshots, experimental inputs and outputs, verification evidence, prompts, model configurations, and offline recomputation scripts.It will retain selection, exclusion, and unresolved-case records and describe the execution environment and external-service configuration.Source: §9 · p. 18