Can we automatically generate formal verifiers from policy text?
Verifier scarcity blocks process verification in most domains. Can language models synthesize correct-by-construction formal checkers directly from natural-language policies, bridging informal rules and rigorous proof?
The chronic obstacle to process verification beyond math and code is verifier scarcity: someone has to write the checker, and most domains lack one. interwhen's second contribution attacks this directly — it synthesizes verifiers automatically from natural-language policy documents. Given a policy stated in prose, the system generates code-based verifiers, and in the strong case produces provably correct verifiers expressed in Lean or z3 (an SMT solver). Once a verifier exists, a language model extracts the verifier's input variables from a partial reasoning trace at runtime, and any formal or code-based verifier can be plugged in.
The significance is the inversion of the usual neuro-symbolic division of labor. Typically the LLM does fuzzy reasoning while a hand-built formal system checks it. Here the LLM is also the bridge that builds and feeds the formal system: it translates prose policy into formal verifier code, and it extracts the formal verifier's inputs from informal trace text. The formal layer (Lean/z3) supplies the provable-correctness guarantee; the LLM supplies the translation between informal policy/trace and formal specification.
This generalizes the reach of process verification from domains with native checkers (theorem proving, code execution) to any domain whose rules can be written down in prose. It connects to the vault's broader thread on offloading reliability to deterministic systems — since Can symbolic solvers fix how LLMs reason about logic?, the established pattern is "LLM formulates, solver executes"; interwhen extends it to "LLM formulates the verifier itself from policy, then solver executes the verifier." Counterpoint and risk: the provable-correctness guarantee covers the verifier's logic, not the LLM's translation of prose into that logic — a mis-synthesized verifier is confidently wrong, so the weakest link migrates from the checker to the prose-to-formal step. Why it matters: it makes formal policy compliance achievable for ordinary agentic tasks without a human writing every verifier.
Inquiring lines that read this note 37
This note is a source for these research framings, grouped by the broader line of inquiry each explores. Scan the bold lines of inquiry; follow any specific question forward.
Why do token-level mechanisms matter for learning to reason? Can local safety checks guarantee system-level behavioral safety?- Should validation responsibility move away from the primary user?
- Can verifier-based objectives preserve reasoning transparency alongside correctness?
- What makes line-by-line proof checking a good fit for AI verification?
- Does internalizing verifiers actually close the generation-verification gap?
- Does the verification gap widen exactly where judgment replaces checkability?
- Can automated tools close the gap between AI generation and verification?
- How does generation-verification asymmetry create the need for verifiable reporting?
- Can verification tools keep pace with AI artifact generation speed?
- How can agents verify research artifacts faster than they generate them?
- Can partial formal verification work without full formalization of language semantics?
- Why does moving verifier synthesis to the LLM extend verification beyond math and code domains?
- Can completeness scaffolding work for domains beyond code verification?
- Can formal verifiers convert statistical semantic claims into deterministic guarantees?
- What breaks when a mis-synthesized verifier runs with high confidence?
- What makes code inspectable feedback more reliable than natural language verification?
- Why can generative verifiers scale verification compute more effectively than fixed-output discriminative models?
- Where does the generation-verification gap appear in test-time compute?
- Do synthetic verification chains from long-CoT models match the quality of human-annotated process labels?
- Who validates task bindings and how is validation checked?
Related concepts in this collection 6
This note in its neighbourhood — explore the map, then jump to a related concept in the list below.
Click a node to walk · click center to open · click Open in graph to see this note in the full knowledge graph
-
Can symbolic solvers fix how LLMs reason about logic?
LLMs excel at understanding natural language but fail at precise logical inference. Can pairing them with deterministic symbolic solvers—using solver feedback to refine attempts—overcome this fundamental weakness?
the "LLM formulates, solver executes" pattern interwhen extends to verifier synthesis
-
Can structured templates replace formal verification for code reasoning?
Formal verification is rigorous but impractical at repository scale. Can natural-language templates with enforced structure provide the same reliability guarantees without the formalization cost? This explores the middle ground between unstructured reasoning and full formalism.
the design-space context: when full formalization is impractical, this synthesizes partial formal checks instead
-
Where do reasoning agents actually fail during long traces?
Does verifying only final answers miss the real sources of failure in multi-step reasoning? This explores whether intermediate process checks reveal errors that outcome-level scoring hides.
the same interwhen framework: synthesized verifiers exist to police the reasoning trace, which is why a verifier must be auto-generated where none exists
-
Can verifiers monitor reasoning without slowing generation down?
Explores whether asynchronous verification can catch reasoning errors while keeping token costs near parity with unmonitored reasoning. Matters because current approaches trade between catching early errors and computational overhead.
enables the deployment of auto-synthesized verifiers: once a Lean/z3 checker exists it can run asynchronously against the trace without slowing generation
-
Can validator consensus guarantee both agreement and semantic correctness?
Explores whether agreement reached by protocol-compliant validators also ensures the agreed outcome is semantically valid, and what assumptions would be needed to make that guarantee hold.
a reason to want such a checker inside a consensus design: an application invariant written as a rule could leave the statistical column; that pairing is a vault inference and not a claim of the Honest Quorum paper
-
What scope should a validator's statistical guarantee actually state?
When an LLM validator is claimed to catch N percent of problems, that number rests on an unstated scope—pointwise, domain-conditional, average-case, or uniform. Why does this distinction matter for safety claims?
the residual: the prose-to-formal translation step this note names would carry its own bound, and a bound needs its scope stated
Related papers in this collection 8
Papers most semantically related to this note, ranked by cosine similarity in the embedding space.
- interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verification
- Complex Logical Instruction Generation
- Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
- Chain of Thoughtlessness? An Analysis of CoT in Planning
- Can Large Language Models Really Improve by Self-critiquing Their Own Plans?
- LLM-as-a-Verifier: A General-Purpose Verification Framework
- Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
- Planning in Strawberry Fields: Evaluating and Improving the Planning and Scheduling Capabilities of LRM o1
Original note title
formal verifiers can be auto-synthesized from natural-language policy documents into lean or z3