System compares ai generated math proofs by their logical steps
ProofDiff: Auditable Argument-Level Comparison of AI-Generated Mathematical Proofs
Artificial Intelligence
Summary
Understanding math proofs isn’t just about the final answer, but the path taken to get there. The authors present ProofDiff, a tool that compares two math proofs by mapping out their reasoning and claims, even if the wording or notation changes. It helps people see if two proofs follow the same logic or if they differ in key steps. ProofDiff is made to assist humans reviewing AI-generated proofs, letting them edit and check the comparison process for accuracy.
What this means in practice
- •For software developers for proof assistants: Integrate tools that help users compare different proof drafts to understand their logical differences even if the proofs use distinct notation or wording.
- •For legal document analysts: Adapt argument-level comparison methods to spot logical structure changes in contracts or legal texts despite paraphrasing or reformatting.
Authors
Matan Tsafrir, Esdras Medeiros, Jorge Poco, Kevin Gomez, Eduardo V. Teixeira, Claudio Silva
Abstract
Mathematical understanding depends on the route from hypotheses to conclusion: how the parts of a proof function and which dependencies carry the argument forward. This structure can persist when wording or notation changes, while a small alteration to a hypothesis or inference can produce a different argument beneath similar prose. Formal verification can establish that a rewrite proves the same theorem, but not whether it follows the same mathematical route. Comparing informal proofs, especially those produced or revised by generative models, therefore requires reconstructing which claims, dependencies, and reasoning steps are preserved, reorganized, or replaced. We present ProofDiff, a system for comparing informal mathematical documents. It is designed to support human review, not to certify mathematical correctness. Given two documents, ProofDiff independently constructs a source-grounded argument map for each and proposes correspondences between the resulting maps. Each map captures the document's claims and reasoning steps and records the typed relations that connect them. An integrated human-review layer allows reviewers to revise the maps and correspondences while preserving an auditable history. Comparing the two argument maps provides a basis for inspecting whether the documents follow the same mathematical route and where their claims or dependencies differ. We demonstrate ProofDiff on four illustrative pairs of AI-generated proofs, ranging from a detailed proof and its concise revision to proofs using different mathematical strategies.