Verification Is Not the Silver Bullet (alperenkeles.com)

This post is a follow-up arguing that while verifiability is important, it is not by itself a panacea for making LLMs reliably autonomous. The author distinguishes human verification (which frames what to check) from computational verification (mechanical tests/provers) and warns that perfect provers — or autoformalization efforts like Harmonic AI’s Aristotle or Math Inc’s Gauss — cannot compensate for imprecise or ambiguous specifications. Even flawless provers won’t help if theorems or formalized specs don’t preserve the original semantics; at every translation step the system must “guess” intent, producing failure modes that verification alone won’t catch. The key proposal is reframing “Verifiability is the Limit” as “Verifiable Progress is the Limit.” Using prime factorization as an example, the author argues that some problems are verifiable (you can check a candidate factorization by multiplication) but lack a useful incremental learning signal: there’s no measure of “how wrong” a guess is, so repeated verification doesn’t yield the comparative feedback that drives model improvement in domains like games or programming. Practical implication: you can’t expect iterative verifier-driven training to crack NP-style problems unless the verifier provides informative, directional feedback or the model uncovers fundamentally new structure. Thus building verifiers is necessary but not sufficient — we must design feedback that produces learning progress, not just binary correctness.