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

cs.SEOct 22, 2026

Beyond Correctness: Attribution of Natural-Language Documentation for Formal Libraries

Authors: Sirui Jiang, Dongming Xiang, Shichao Wu, Yuxuan Zhou, Yihong Wu, Fangze Zhu, Wang Lin, Guanjun Liu

Organizations: Zhejiang Sci-Tech University, China · Zhejiang Gongshang University, China · Tongji University, China

Abstract

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.

Figures & tables

Measure	Unit of decision	Reference	Question answered	Can reject Figure 1 statements
Provability ( Ma et al., 2025 )	Individual property	Original target	Can the property be proved?	✗
Mutation discrimination ( Endres et al., 2024 ; Amaral et al., 2026 ; Goldweber et al., 2024 )	Property or whole specification	Selected code mutants	Which tested implementations does it rule out?
Vacuity and semantic dependence ( Beer et al., 2001 ; Podgurski and Clarke, 1990 ; Chockler et al., 2008 )	Property or program part	Changes to a subformula or program part	Does the conclusion depend on the changed part?	✗
Document–code equivalence ( Eghbali et al., 2026 ; Zeng et al., 2026 )	Entire document or specification	Overall behavior of the original target	Do the two describe the same behavior?	✗
Source support and consistency ( Rashkin et al., 2023 ; Panthaplackel et al., 2021 ; Sun et al., 2024 )	Sentence or comment	Source text or code	Is the statement supported and consistent?	✗
Attribution (ours)	Individual statement	Implementations under the fixed interface	Does it add behavioral information beyond the interface?	✓

Table 1. Attribution compared with existing measures. ✓ guaranteed; depends on the selected variants; ✗ not guaranteed.

Figure 3. The DocAuth workflow The workflow has three stages. During candidate generation, an LLM reads the formal target function and proposes candidate properties. The candidate check first identifies non-attributable properties through an erasure proof, then obtains a target proof and an interface-conforming witness for the remaining properties; these two items form the attribution evidence. Properties that pass the check are rendered as natural-language sentences, from which formal properties are recovered by back-translation and subjected to the sentence recheck; only sentences that pass both checks are published to developers, and everything else is discarded.

	Qwen2.5-7B	DeepSeek-v4-flash	GPT-5.6-terra	Human-written
Properties checked	1,743	2,030	2,090	1,068
Checks completed	939	1,215	1,371	466
❶ Attributable	461 (49.1%)	921 (75.8%)	1,209 (88.2%)	409 (87.8%)
False for the target	373 (39.7%)	143 (11.8%)	27 (2.0%)	0 (0.0%)
❷ Non-attributable	80 (8.5%)	77 (6.3%)	72 (5.3%)	20 (4.3%)
❸ No witness found	25 (2.7%)	74 (6.1%)	63 (4.6%)	37 (7.9%)

Table 2. Outcomes of the properties checked on

150

functions

Property source	Attributable	No witness found	Non-attributable
Qwen2.5-7B	68/123 (55.3 %)	1/6 (16.7 %)	0/16
DeepSeek-v4-flash	204/304 (67.1 %)	4/21 (19.0 %)	0/14
GPT-5.6-terra	264/401 (65.8 %)	4/19 (21.1 %)	0/10
Human-written	78/120 (65.0 %)	0/13 (0.0 %)	0/8
Total	614/948 (64.8 %)	9/59 (15.3 %)	0/48

Table 3. Change detection by property source and check outcome

Generator model	Method	Published	Attributable	Cross-model	Interface-only	Interface-only, equivalent to $\psi$
Qwen2.5-7B	Baseline	575	247	43.0%	26.1%	20.2%
	+ LLM judge	404	217	53.7%	34.2%	26.5%
	Truth check	376	299	79.5%	62.5%	43.9%
	+ LLM judge	359	290	80.8%	63.5%	44.8%
	+ mutation filter	265	229	86.4%	64.5%	44.2%
	DocAuth	359	317	88.3%	68.0%	46.8%

Table 4. Attributable sentences and attribution rates by generator model and reassessment condition

Panel of Figure 6 — Figure 6. Sentence attribution rates, pooled over the three models Grouped bar chart. The horizontal axis shows the three reassessment conditions: cross-model, interface-only, and interface-only with equivalence to psi. Each group has six bars, for the baseline, the baseline with LLM judging, truth checking, truth checking with LLM judging, truth checking with mutation filtering, and \tool; error bars are 95% bootstrap intervals clustered by target function. \tool's bar is the tallest in all three groups, at 94.7%, 75.7%, and 52.7%, respectively. Table~\ref{tab:independent} gives the values for each generator model.

Method	Nothing published	${\geq}1$ attributable	${\geq}2$ attributable	$4$ attributable	Attributable per document	Attribution rate
Baseline	0.7%	83.3%	65.8%	8.0%	1.90	49.7%
Truth check	16.9%	79.3%	72.0%	30.9%	2.40	82.9%
+ mutation filter	36.4%	62.4%	55.6%	26.4%	1.90	92.0%
DocAuth	18.7%	80.9%	74.7%	40.9%	2.60	94.7%

Table 5. Per-function delivery

Panel of Figure 7 — Figure 7. Effects of the candidate budget, the search scope, and the number of sentences per function Four line plots in one row. (a) As the candidate budget grows, the share of attributable properties falls for all four property sources. (b) The number of properties still without a witness when the search is limited to a prefix of the alternative implementations drops sharply at the second alternative and keeps falling to the no-witness-found count of the full search. (c, d) With published sentences truncated per function, DocAuth's attribution rate stays above that of truth checking, and the number of attributable sentences delivered by all three methods grows with the number of sentences per function.

Property source	Properties checked	Functions covered	Coverage
Qwen2.5-7B	1,743	114/150	76.0%
DeepSeek-v4-flash	2,030	127/150	84.7%
GPT-5.6-terra	2,090	123/150	82.0%
Human-written	1,068	105/150	70.0%

Table 6. Function coverage by property source

Panel of Figure 8 — Figure 8. Check outcomes and reasons for unresolved outcomes by property source Each panel has four stacked percentage bars for Qwen2.5-7B, DeepSeek-v4-flash, GPT-5.6-terra, and human-written properties. Panel (a) partitions all checked properties into attributable, false for the target, non-attributable, no witness found, and unresolved. Panel (b) partitions each source's unresolved properties into missing target proofs, missing dependencies or erasure-environment problems, evaluation failures or unmet premises, and other incomplete checks.

Figure 9. Distribution of token usage and total time per function Three violin plots show the distributions of input tokens, output tokens, and total time over the 149 functions. Each plot has a quartile bar and a median dot in the middle, and each function is drawn as a point: dark blue for functions that publish sentences and gray for those that publish nothing. Functions that publish nothing cluster at the low end of total time and also use the fewest input tokens.

Text Generation

Text generation studies methods for producing coherent, useful language from prompts, data, and dialogue context.

See all 424 papers

Oct 14, 2026

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.

Anna Mei, Michael R. Douglas

Harvard University · CMSA, Harvard University and AletheAI, Inc

Formal Verification Autoformalization LLM-as-a-Judge

Ask PDF

Oct 22, 2026

PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean

Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.

Jiyuan Tan, Jose Blanchet, Vasilis Syrgkanis

Stanford University

Autoformalization Formal Verification Lean Theorem Proving

Ask PDF

Sep 30, 2026

Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization

We present FYAN, a human--AI harness for document-level mathematical formalization. Rather than treating theorems in isolation, FYAN coordinates an end-to-end workflow spanning specification, proof planning, logical review, Lean proof construction, knowledge curation, and validation, with support for independent supervision and human guidance. A central component is evidence-grounded semantic auditing, which assesses whether formal statements faithfully preserve their informal specifications. A language model constructs structured evidence over local correspondences, omissions, scope, and logical relations, while a deterministic validator checks this evidence and produces reproducible judgments. When a substantive but admissible deviation is accepted, FYAN requires an explicit proof-transfer obligation connecting the formal statement back to a source-facing interpretation. With the same model (DeepSeek-V4.1-Flash) in every stage, FYAN proves 86 of 143 FormalTCS theorems under a strict Lean check, against 69 for a general agent harness, and raises the natural-language proof score from 0.501 to 0.851. On ConsistencyCheck, its semantic audit catches more inconsistent statements than a direct LLM judge, both on labels verified against the source (recall 0.777 vs. 0.636) and on the original labels (0.873 vs. 0.820), and localizes each mismatch it reports to a specific hypothesis, conclusion, or scope. FYAN also built ODENumLib, a 9,355-line Lean library for the numerical analysis of ordinary differential equation.

Wei Zhao, Yangshuo Zou, Chengxiang Ding +5

School of Mathematical Sciences, Shanghai Jiao Tong University, Shanghai 200240, China · University of California, Berkeley, CA 94720, USA · Zhiyuan College, Shanghai Jiao Tong University, Shanghai 200240, China +4

Automated Theorem Proving Human-in-the-Loop AI Lean Theorem Proving Autoformalization

Ask PDF

Abstract

Text Generation

Explore similar work

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean

Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization