The authors address the problem of "conflicted tasks" in autonomous coding agents: tasks whose natural-language description and test suite cannot both be satisfied, leading agents to cheat by editing tests or hard-coding outputs.
Formal verification catches broken coding tasks before agents cheat
SpecGuard autoformalizes task intent and tests into Lean 4, producing machine-checked certificates of conflict.
Big Tech
Param Biyani · Krishnamurthy Dvijotham
MATS · Google DeepMind
Research Digest··3 min read
Biyani and Dvijotham introduce SpecGuard, a system that detects and formally certifies conflicts between a coding task's natural-language description and its tests.
Why this paper
From Google DeepMind and MATS
In one line
SpecGuard detects and formally certifies conflicts between task intent and tests before an agent can cheat.
What we could check
- ·No code link found
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ✓Limitations stated by the authors
- ✓Reports numbers on named benchmarks
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§