Formal methods clarify automated fact checking and accountability
SoK: Formal Methods for Fact-Checking and Information Integrity
Computation and LanguageComputers and SocietyLogic in Computer Science
Summary
Fact-checking systems often give simple true or false answers but don’t explain exactly how they reached those conclusions or what evidence supports them. The authors look at ways formal methods—strict mathematical techniques—can provide clear evidence for fact-checkers’ decisions. They organize 121 studies by what parts of fact-checking are formalized, finding some important gaps such as defining correctness for certain steps. Their work highlights what research exists, what is missing, and suggests next steps to make fact-checking more transparent and reliable.
What this means in practice
- •For fact-checking teams: Provide clearer evidence and explanations for fact-checking decisions to meet growing regulatory demands for auditability.
- •For content moderation teams: Use formal verification methods to improve the reliability and transparency of automated checks on content claims.
A survey. It maps existing work.
Authors
Nikolaos Kekatos, Theodoros Nestoridis, Charalampos Bratsas, Charalampos Dimoulas, Georgios Konstantinidis, Georgios Malogiannis, Michael Sirivianos, Andreas Veglis
Abstract
An automated fact-checking system returns a label: the claim is true, or it is false. In many such systems the verdict remains the primary output. What is generally missing is a record of which document settled the question, of what would have had to be different for the verdict to change, or of whether the same claim, reworded, would have been judged the same way. We call the missing piece a warrant: a separate statement of what was guaranteed and on what grounds. Formal methods produce evidence of this kind, and regulation is beginning to ask for it, since the Digital Services Act and the AI Act both call for auditable evidence about how systems behave. Surveys of automated fact-checking are usually organised by pipeline stage, and treat logic as one technique among many. We organise the field by what is being formalised instead, which gives five levels: the claim, the reasoning, the system doing the checking, the ecosystem the claim spreads through, and the regulatory obligation. Sorting 121 works into those levels, two patterns stand out. Most of the relevant formal machinery already exists, but it was built for other domains and has rarely been applied here, and the gap is widest for verifying the checking system itself. Several stages of the routine professional fact-checkers follow also have no stated correctness criterion, and two of them, writing a claim in checkable form and correcting a verdict already published, are not formally specified in any work we coded. We close with open problems, each with a suggested first step.