Formal Verification

Opening — Why this matters now Neural theorem proving has entered its industrial phase. With reinforcement learning pipelines, synthetic data factories, and search budgets that would make a chess engine blush, models like DeepSeek‑Prover‑V1.5 are widely assumed to have internalized everything there is to know about formal proof structure. This paper politely disagrees. Under tight inference budgets—no massive tree search, no thousand-sample hail‑Mary—the author shows that simple, almost embarrassingly old‑fashioned structural hints still deliver large gains. Not new models. Not more data. Just better scaffolding. ...

If you strip away the rhetoric about “thinking” machines and “cognitive” agents, most of today’s agentic AIs still boil down to something familiar from the 1950s: automata. That’s the thesis of Are Agents Just Automata? by Koohestani et al. (2025), a paper that reinterprets modern agentic AI through the lens of the Chomsky hierarchy—the foundational classification of computational systems by their memory architectures. It’s an argument that connects LLM-based agents not to psychology, but to formal language theory. And it’s surprisingly clarifying. ...