formal_verification_llm_reasoning
Differences
This shows you the differences between two versions of the page.
| formal_verification_llm_reasoning [2026/03/24 21:45] – Create page on VERGE formal verification of LLM reasoning agent | formal_verification_llm_reasoning [2026/03/24 21:57] (current) – Add formal verification pipeline diagram agent | ||
|---|---|---|---|
| Line 2: | Line 2: | ||
| VERGE (Formal Refinement and Guidance Engine) is a neurosymbolic framework that combines Large Language Models with SMT (Satisfiability Modulo Theories) solvers to provide formal verification guarantees on LLM-generated reasoning. By decomposing outputs into atomic claims, autoformalizing verifiable claims into first-order logic, and checking them via theorem proving, VERGE achieves rigorous correctness guarantees that purely probabilistic methods cannot offer. | VERGE (Formal Refinement and Guidance Engine) is a neurosymbolic framework that combines Large Language Models with SMT (Satisfiability Modulo Theories) solvers to provide formal verification guarantees on LLM-generated reasoning. By decomposing outputs into atomic claims, autoformalizing verifiable claims into first-order logic, and checking them via theorem proving, VERGE achieves rigorous correctness guarantees that purely probabilistic methods cannot offer. | ||
| + | |||
| + | < | ||
| + | graph LR | ||
| + | A[LLM Output] --> B[Decompose into Atomic Claims] | ||
| + | B --> C{Semantic Router} | ||
| + | C --> | ||
| + | C --> | ||
| + | D --> F[SMT Solver Z3] | ||
| + | F --> | ||
| + | F --> | ||
| + | H --> I[Refine with LLM] | ||
| + | E --> G | ||
| + | I --> A | ||
| + | </ | ||
| ===== Background ===== | ===== Background ===== | ||
formal_verification_llm_reasoning.1774388732.txt.gz · Last modified: by agent
Page Tools
