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 use this note as a source 26
This note is a source for these synthesized inquiries. Follow a line forward into its question, or open it to trace back to all of its sources.
- Why do tokens need validators while commodities need standardization?
- Should validation responsibility move away from the primary user?
- Can we verify fabricated text without redesigning the generation process?
- How can we verify outputs from systems that generate without grounding?
- Does internalizing verifiers actually close the generation-verification gap?
- Does Promptbreeder actually escape the generation-verification gap constraints?
- Does the verification gap widen exactly where judgment replaces checkability?
- How should harness infrastructure validate code that agents generate themselves?
- Why do AI agents fail at verification but succeed at generation?
- Can automated tools close the gap between AI generation and verification?
- How does generation-verification asymmetry create the need for verifiable reporting?
- Can partial formal verification work without full formalization of language semantics?
- What breaks when a mis-synthesized verifier runs with high confidence?
- Why does moving verifier synthesis to the LLM extend verification beyond math and code domains?
- Why can generative verifiers scale verification compute more effectively than fixed-output discriminative models?
- Can verification tools keep pace with AI artifact generation speed?
- Do synthetic verification chains from long-CoT models match the quality of human-annotated process labels?
- Can verifier output replace ground-truth answers as the asymmetric information source?
- Can verifier-based objectives preserve reasoning transparency alongside correctness?
- How can verifiers check policy compliance in agentic reasoning tasks?
- Why does self-verification fail but external process verification work?
- What reasoning tasks are actually checkable through process verification?
- How do verifier-free RL patterns differ from traditional RLHF approaches?
- Can completeness scaffolding work for domains beyond code verification?
- Why do model-based verifiers introduce reward hacking and compute overhead?
- Where does the generation-verification gap appear in test-time compute?
Related concepts in this collection 4
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
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?
- Planning in Strawberry Fields: Evaluating and Improving the Planning and Scheduling Capabilities of LRM o1
- Understanding Tool-Integrated Reasoning
- How Many Instructions Can LLMs Follow at Once?
Original note title
formal verifiers can be auto-synthesized from natural-language policy documents into lean or z3