"My pipeline has four stages: generate, score, verify, and despair. The first three are automated. The fourth activates when the type checker says 'sorry is not a proof.'"
A Verification Pipeline That Has Seen Things
The preceding sections introduced the components: chain-of-thought (CoT) generation (Section 29.1), process reward model (PRM) scoring (Section 29.2), and formal verification (Section 29.3). This section assembles them into a complete pipeline that solves a mathematical optimization problem with graduated levels of confidence. The pipeline generates multiple reasoning chains, ranks them by step-level PRM scores, translates the best candidates into Lean 4 (an interactive theorem prover whose type system encodes mathematical logic, so any program that type-checks constitutes a machine-verified proof) sketches, and attempts formal verification of the critical derivation steps. The result is not a binary "verified or not" but a structured verification report that quantifies exactly which parts of the derivation are machine-checked, which are PRM-scored, and which are unverified. This recipe is directly applicable to any scientific workflow where reasoning correctness matters.
1. Architecture of the Verified Reasoning Pipeline
When a language model derives that a new drug candidate binds 10x more strongly than expected, would you stake a \$2 million clinical trial on that conclusion without a machine-checked proof of every algebraic step? This pipeline provides exactly that assurance, in four stages that build successive layers of confidence, as illustrated in Figure 29.4:
A verified reasoning pipeline takes a natural-language problem statement as input and produces not just an answer but a structured certificate documenting correctness evidence for every derivation step. Large language model (LLM)-generated reasoning can contain subtle logical errors that look plausible to human reviewers. Layering statistical scoring (PRM) with formal proof checking (Lean 4) catches errors that either method alone would miss. The pipeline treats each reasoning step as an independent claim, scores it for plausibility, and routes low-confidence claims to a theorem prover that confirms or refutes them mechanically. Use this pipeline whenever an undetected reasoning error would be costly (scientific publications, safety-critical engineering calculations, regulatory submissions). For low-stakes or exploratory reasoning where speed matters more than guarantees, a single LLM call with manual review is more practical.
- Generate: produce \(N\) candidate solutions using chain-of-thought prompting with extended thinking.
- Score: evaluate each candidate step-by-step using a process reward model, identifying the strongest chains and the weakest steps.
- Verify: translate the top-scoring candidates into Lean 4 proof sketches and attempt formal verification of as many steps as possible.
- Report: produce a structured output that combines the informal solution, the PRM scores, and the formal verification status into a single confidence assessment.
Each stage filters and enriches its predecessor's output: generation explores broadly (many candidates, high temperature), scoring narrows to the most promising chains, and verification provides the strongest guarantees on the best candidate. This cascade mirrors the funnel architecture of information retrieval (recall, rank, re-rank) and the experiment design pipeline from Chapter 46: Automated Experiment Design. In short: generate broadly, score narrowly, verify only what the scores distrust.
Mental Model
Think of the pipeline as a hiring process for job candidates. Stage 1 (Generate) is posting the job listing and collecting many resumes. Stage 2 (Score) is a recruiter screening each resume line by line, flagging weak spots and ranking applicants. Stage 3 (Verify) is calling references and running background checks, but only for the top candidates and only on the claims that looked questionable. Stage 4 (Report) is the hiring committee's summary: "This candidate's technical skills are reference-verified, their education is confirmed, their hobbies section was not checked but looks fine." Just as you would not background-check every line of every resume (too expensive) but you would always check the credentials that matter most, the pipeline concentrates formal verification on the reasoning steps most likely to contain errors.
import anthropic
import json
import re
import subprocess
import tempfile
import os
from dataclasses import dataclass, field
from typing import Optional
client = anthropic.Anthropic()
@dataclass
class ReasoningStep:
"""A single step in a reasoning chain, with scores."""
text: str
prm_score: float = 0.0
lean_verified: Optional[bool] = None # None = not attempted
lean_code: str = ""
@dataclass
class ScoredChain:
"""A complete reasoning chain with per-step scores."""
steps: list[ReasoningStep]
raw_text: str
min_score: float = 0.0
product_score: float = 0.0
verification_confidence: float = 0.0
@dataclass
class VerificationReport:
"""Final output of the verified reasoning pipeline."""
problem: str
best_chain: ScoredChain
answer: str
n_candidates_generated: int
n_steps_verified: int
n_steps_total: int
overall_confidence: str # "formally_verified", "prm_high", "prm_low"
details: dict = field(default_factory=dict)
ReasoningStep carries a PRM score and optional Lean verification status; ScoredChain aggregates per-step results with minimum and product scores; VerificationReport combines step-level information into an overall confidence assessment.2. Stage 1: Generate Candidate Solutions
The generation stage uses extended thinking (a mode that allocates additional internal reasoning tokens before the model produces its visible answer) to produce diverse, high-quality reasoning chains. We sample \(N\) candidates with varying thinking budgets to encourage diversity: some chains will use standard approaches, while others, given more internal reasoning tokens, may discover creative shortcuts.
def generate_candidates(
problem: str,
n_candidates: int = 6,
thinking_budget: int = 10000
) -> list[str]:
"""Generate N candidate reasoning chains using extended thinking.
Uses varying temperatures to produce diverse solution strategies.
Each candidate is a complete step-by-step derivation.
"""
candidates = []
for i in range(n_candidates):
# Vary temperature slightly for diversity
# Extended thinking uses budget_tokens instead of temperature
budget = thinking_budget + (i * 1000) # more thinking for later candidates
response = client.messages.create(
model="claude-sonnet-4-20250514",
max_tokens=16000,
thinking={
"type": "enabled",
"budget_tokens": min(budget, 16000)
},
messages=[{
"role": "user",
"content": f"""Solve this optimization problem step by step.
Number each step clearly (Step 1, Step 2, ...).
Show all mathematical work. Verify your answer.
Problem: {problem}"""
}]
)
# Extract the text response (not the thinking block)
for block in response.content:
if block.type == "text":
candidates.append(block.text)
break
return candidates
def split_into_steps(chain: str) -> list[str]:
"""Split a reasoning chain into individual numbered steps."""
# Match "Step N:" or "N." or "N)" patterns
parts = re.split(r'(?=(?:Step\s+)?\d+[\.\):])', chain)
steps = [p.strip() for p in parts if p.strip() and len(p.strip()) > 20]
if len(steps) <= 1:
# Fallback: split on double newlines
steps = [p.strip() for p in chain.split('\n\n')
if p.strip() and len(p.strip()) > 20]
return steps
budget_tokens values. Higher budgets allow more internal reasoning, increasing the chance of discovering correct (and sometimes creative) derivation paths. The split_into_steps helper parses numbered steps using regex with a fallback to paragraph splitting.3. Stage 2: Score with Process Reward Model
The scoring stage evaluates each step in each candidate chain. We use the LLM-as-PRM approach from Section 29.2, scoring each step on correctness, logical validity, and mathematical rigor. The output is a ranked list of chains with per-step scores.
def score_step(
problem: str,
preceding: list[str],
current: str,
domain: str = "mathematics"
) -> float:
"""Score a single reasoning step using an LLM as a process reward model.
Returns a confidence score between 0.0 and 1.0.
"""
context = "\n".join(preceding) if preceding else "(beginning of solution)"
response = client.messages.create(
model="claude-sonnet-4-20250514",
max_tokens=256,
temperature=0.0,
messages=[{
"role": "user",
"content": f"""Evaluate this {domain} reasoning step for correctness.
Problem: {problem}
Previous steps:
{context}
Current step to evaluate:
{current}
Rate correctness from 0.0 to 1.0. Respond with ONLY a JSON object:
{{"score": , "issue": ""}}"""
}]
)
try:
result = json.loads(response.content[0].text)
return float(result.get("score", 0.5))
except (json.JSONDecodeError, ValueError):
return 0.5
def score_chain(problem: str, chain_text: str) -> ScoredChain:
"""Score an entire reasoning chain step by step."""
step_texts = split_into_steps(chain_text)
steps = []
scores = []
for i, step_text in enumerate(step_texts):
preceding = [s.text for s in steps]
score = score_step(problem, preceding, step_text)
steps.append(ReasoningStep(text=step_text, prm_score=score))
scores.append(score)
product = 1.0
for s in scores:
product *= s
return ScoredChain(
steps=steps,
raw_text=chain_text,
min_score=min(scores) if scores else 0.0,
product_score=product,
verification_confidence=0.0
)
def rank_candidates(
problem: str,
candidates: list[str]
) -> list[ScoredChain]:
"""Score and rank all candidate chains by PRM quality."""
scored = [score_chain(problem, c) for c in candidates]
# Sort by minimum step score (weakest-link criterion)
scored.sort(key=lambda c: c.min_score, reverse=True)
return scored
score_step evaluates one step against its predecessors and returns a 0.0 to 1.0 confidence score. rank_candidates sorts chains by their weakest step (minimum score), applying a weakest-link criterion: because a single erroneous step can invalidate an entire derivation, the chain's reliability is bounded by its least confident step.Formal verification is expensive (each Lean compilation takes seconds to minutes, and autoformalization, where a language model translates informal mathematics into formal proof code, may require multiple attempts). The PRM scores tell us exactly where to focus: steps with low PRM scores are the most likely to contain errors and the most valuable to verify formally. A step with PRM score 0.99 is almost certainly correct and formal verification adds little value. A step with PRM score 0.6 is suspicious and worth the verification cost. This targeted strategy can typically reduce the number of Lean compilations by 60-80% compared to verifying every step, while catching a comparable proportion of errors. The principle is identical to risk-based testing in software engineering (Chapter 18): concentrate quality assurance effort where the risk is highest.
Common Misconception
A common misconception is that a pipeline reporting "formally_verified" confidence means the entire proof has been checked as a single end-to-end logical chain, the way a mathematician would verify a proof from axioms to conclusion. In reality, each step is formalized and verified independently: the Lean type checker confirms that step 3's claim follows from its stated premises, but it does not verify that those premises actually match the output of step 2 in the informal text. Gaps between steps (unstated assumptions, minor reformulations, implicit variable substitutions) are not covered by the formal verification. The pipeline's confidence label reflects the per-step verification status, not a monolithic proof certificate, and users should review the step boundaries for logical coherence even when every individual step passes.
4. Stage 3: Formal Verification of Critical Steps
The verification stage translates the top-scoring chain's critical steps into Lean 4 and attempts formal proof. We focus verification on the mathematical core of the derivation: the steps that establish key equalities, inequalities, or logical implications. Purely expository steps ("we want to find the minimum") are not worth formalizing.
def check_lean_code(lean_code: str, timeout: int = 30) -> dict:
"""Check Lean 4 code for type correctness.
Returns a dict with success status and error details.
Requires Lean 4 installed and a project with Mathlib.
"""
with tempfile.NamedTemporaryFile(
mode='w', suffix='.lean', delete=False
) as f:
f.write("import Mathlib.Tactic\n\n" + lean_code)
tmp = f.name
try:
result = subprocess.run(
["lake", "env", "lean", tmp],
capture_output=True, text=True, timeout=timeout
)
return {
"success": result.returncode == 0,
"errors": result.stderr
}
except (subprocess.TimeoutExpired, FileNotFoundError) as e:
return {"success": False, "errors": str(e)}
finally:
os.unlink(tmp)
def formalize_step(
problem: str,
step: ReasoningStep,
preceding_steps: list[ReasoningStep],
max_attempts: int = 3
) -> ReasoningStep:
"""Attempt to formalize and verify a single reasoning step in Lean 4.
Translates the step to Lean, checks it, and retries with error
feedback on failure.
"""
context = "\n".join(s.text for s in preceding_steps)
errors_history = []
for attempt in range(max_attempts):
error_hint = ""
if errors_history:
error_hint = f"\n\nPrevious attempt errors:\n" + "\n".join(errors_history[-2:])
response = client.messages.create(
model="claude-sonnet-4-20250514",
max_tokens=1024,
temperature=0.2 + 0.1 * attempt,
messages=[{
"role": "user",
"content": f"""Formalize this mathematical reasoning step as a
Lean 4 lemma. Use Mathlib tactics (ring, linarith, norm_num, simp, omega).
Output ONLY valid Lean 4 code.
Problem context: {problem}
Previous reasoning:
{context}
Step to formalize:
{step.text}
{error_hint}"""
}]
)
lean_code = response.content[0].text.strip()
# Strip markdown fences
if "```" in lean_code:
blocks = lean_code.split("```")
for block in blocks:
if "theorem" in block or "lemma" in block or "example" in block:
lean_code = block.replace("lean", "").strip()
break
result = check_lean_code(lean_code)
if result["success"]:
step.lean_verified = True
step.lean_code = lean_code
return step
else:
errors_history.append(result["errors"][:300])
step.lean_verified = False
step.lean_code = lean_code # keep last attempt for debugging
return step
def verify_critical_steps(
problem: str,
chain: ScoredChain,
prm_threshold: float = 0.85
) -> ScoredChain:
"""Formally verify steps with PRM scores below a threshold.
Steps scoring above the threshold are considered reliable enough
to skip formal verification, reducing the computational cost.
Args:
problem: The original problem statement
chain: A scored reasoning chain
prm_threshold: Steps with scores below this are sent to Lean
Returns:
The chain with updated verification status on critical steps
"""
n_verified = 0
n_attempted = 0
for i, step in enumerate(chain.steps):
if step.prm_score < prm_threshold:
n_attempted += 1
preceding = chain.steps[:i]
formalize_step(problem, step, preceding)
if step.lean_verified:
n_verified += 1
total_steps = len(chain.steps)
high_prm_steps = sum(1 for s in chain.steps if s.prm_score >= prm_threshold)
formally_verified = sum(1 for s in chain.steps if s.lean_verified is True)
# Confidence: formally verified steps count fully,
# high-PRM steps count at their PRM score
confidence = (
formally_verified +
sum(s.prm_score for s in chain.steps if s.prm_score >= prm_threshold)
) / max(total_steps, 1)
chain.verification_confidence = confidence
return chain
check_lean_code writes a temporary .lean file importing Mathlib (Lean 4's community-maintained library of formalized mathematics, providing thousands of theorems and tactics) and runs the type checker. formalize_step retries up to three times with increasing temperature and error feedback. verify_critical_steps routes only steps below the PRM threshold to Lean, concentrating expensive compilation on the weakest links.5. Stage 4: Assemble the Report
The final stage combines all the information from the pipeline into a structured report. The report assigns an overall confidence level based on the verification results and provides actionable detail for each step.
def build_report(
problem: str,
chain: ScoredChain,
n_candidates: int
) -> VerificationReport:
"""Assemble the final verification report."""
n_verified = sum(1 for s in chain.steps if s.lean_verified is True)
n_total = len(chain.steps)
# Extract the final answer from the last step
answer = chain.steps[-1].text if chain.steps else "No answer found"
# Determine overall confidence level
# A step is "covered" if it is Lean-verified or scored above the
# PRM threshold, meaning formal verification was not attempted.
n_uncovered = sum(
1 for s in chain.steps
if s.lean_verified is not True and s.prm_score < 0.85
)
if n_uncovered == 0 and n_verified > 0:
confidence = "formally_verified"
elif n_uncovered == 0:
confidence = "prm_high"
else:
confidence = "prm_low"
return VerificationReport(
problem=problem,
best_chain=chain,
answer=answer,
n_candidates_generated=n_candidates,
n_steps_verified=n_verified,
n_steps_total=n_total,
overall_confidence=confidence,
details={
"step_scores": [
{
"step": i + 1,
"prm_score": round(s.prm_score, 3),
"lean_verified": s.lean_verified,
"text_preview": s.text[:80]
}
for i, s in enumerate(chain.steps)
],
"min_prm_score": round(chain.min_score, 3),
"product_prm_score": round(chain.product_score, 6),
"verification_confidence": round(chain.verification_confidence, 3)
}
)
build_report function classifies the chain as "formally_verified" (every below-threshold step verified by Lean and all others scored above threshold), "prm_high" (all steps scored above threshold so none required formal verification), or "prm_low" (at least one below-threshold step that could not be formally verified). Per-step detail is preserved in the details dictionary for downstream inspection.When the pipeline assigns a "prm_low" confidence label, the report identifies the specific steps that failed both PRM scoring and formal verification. The recommended workflow is to treat these steps as hypotheses requiring manual review: inspect the flagged step's text alongside the Lean error output (preserved in lean_code), determine whether the error is a formalization failure (the mathematics is correct but the translation to Lean was wrong) or a genuine reasoning error (the mathematics itself is flawed), and either rephrase the step for another verification attempt or correct the reasoning and re-run the pipeline. Without this triage step, the pipeline reports a problem but does not resolve it.
6. The Complete Pipeline
With all four stages defined, the complete pipeline is a direct composition. We apply it to a mathematical optimization problem that exercises each stage: generating candidate solutions, scoring them for correctness, and verifying the critical algebraic steps.
def verified_reasoning_pipeline(
problem: str,
n_candidates: int = 6,
thinking_budget: int = 10000,
prm_threshold: float = 0.85,
domain: str = "mathematics"
) -> VerificationReport:
"""Complete verified reasoning pipeline.
Generates candidates, scores them step-by-step, verifies
critical steps formally, and produces a structured report.
Args:
problem: The mathematical problem to solve
n_candidates: Number of candidate chains to generate
thinking_budget: Token budget for extended thinking
prm_threshold: PRM score below which formal verification is attempted
domain: Problem domain (for PRM prompting)
Returns:
VerificationReport with confidence assessment
"""
print(f"Stage 1: Generating {n_candidates} candidate solutions...")
candidates = generate_candidates(problem, n_candidates, thinking_budget)
print(f" Generated {len(candidates)} candidates")
print("Stage 2: Scoring candidates with process reward model...")
ranked = rank_candidates(problem, candidates)
best = ranked[0]
print(f" Best chain: {len(best.steps)} steps, "
f"min PRM score = {best.min_score:.3f}")
# Show step-level scores for the best candidate
for i, step in enumerate(best.steps):
status = "OK" if step.prm_score >= prm_threshold else "CHECK"
print(f" Step {i+1} [{status}] PRM={step.prm_score:.3f}: "
f"{step.text[:60]}...")
print("Stage 3: Formally verifying critical steps...")
best = verify_critical_steps(problem, best, prm_threshold)
n_verified = sum(1 for s in best.steps if s.lean_verified is True)
n_attempted = sum(1 for s in best.steps if s.lean_verified is not None)
print(f" Verified {n_verified}/{n_attempted} attempted steps")
print("Stage 4: Assembling verification report...")
report = build_report(problem, best, n_candidates)
print(f" Overall confidence: {report.overall_confidence}")
return report
# Example: solve and verify a mathematical optimization problem
PROBLEM = """
Find the minimum value of the function f(x, y) = x^2 + y^2 + 2/x + 2/y
for x > 0 and y > 0.
Show that the minimum exists, find the critical point, verify it is
a minimum (not a maximum or saddle point), and compute the minimum value.
"""
# Uncomment to run the full pipeline:
# report = verified_reasoning_pipeline(PROBLEM, n_candidates=4)
# print(f"\nAnswer: {report.answer}")
# print(f"Steps: {report.n_steps_total}")
# print(f"Verified: {report.n_steps_verified}")
# print(f"Confidence: {report.overall_confidence}")
# print(f"\nDetails:")
# for step_info in report.details["step_scores"]:
# print(f" Step {step_info['step']}: "
# f"PRM={step_info['prm_score']}, "
# f"Lean={'yes' if step_info['lean_verified'] else 'no' if step_info['lean_verified'] is not None else 'skip'}")
A computational chemistry team uses the pipeline to verify a binding affinity derivation. The problem: given the dissociation constant \(K_d\) (the concentration at which half of the protein binding sites are occupied by the ligand) and the protein-ligand interaction energy \(\Delta G\), derive the relationship \(\Delta G = RT \ln(K_d)\) and compute the expected binding affinity at 310 K (body temperature). The pipeline generates 6 candidate derivations, scoring each step for thermodynamic correctness. The PRM flags a common error: candidates that confuse \(\ln\) and \(\log_{10}\), producing off-by-a-factor-of-2.303 results. The formal verification stage confirms the correct derivation by checking the dimensional consistency of each term (energy units on the left, dimensionless argument to the logarithm on the right). The final report indicates that 4 of 5 derivation steps are formally verified, with one step (the numerical substitution) verified only by PRM scoring. This partial verification is sufficient to trust the derivation while explicitly marking the unverified numerical computation for manual checking. The same pipeline structure applies to the pharmacokinetic modeling workflows in Chapter 48: Discovery AI for Biology and Medicine.
7. Extending the Pipeline: Scientific Domains
The pipeline as built targets mathematical optimization, but the architecture generalizes to any domain where reasoning steps can be evaluated and (partially) verified. Three extensions are particularly relevant for scientific discovery:
Physical Units Verification
A lightweight alternative to full Lean verification is dimensional analysis checking. Every equation in physics must be dimensionally consistent: you cannot add meters to seconds. A dimensional analysis checker can flag errors that the PRM misses (e.g., a step that produces the right numerical answer but with wrong units):
from dataclasses import dataclass
@dataclass
class Dimension:
"""Physical dimensions represented as exponent vector [M, L, T, K, mol]."""
mass: int = 0
length: int = 0
time: int = 0
temperature: int = 0
amount: int = 0
def __mul__(self, other: "Dimension") -> "Dimension":
return Dimension(
self.mass + other.mass,
self.length + other.length,
self.time + other.time,
self.temperature + other.temperature,
self.amount + other.amount
)
def __truediv__(self, other: "Dimension") -> "Dimension":
return Dimension(
self.mass - other.mass,
self.length - other.length,
self.time - other.time,
self.temperature - other.temperature,
self.amount - other.amount
)
def __eq__(self, other: "Dimension") -> bool:
return (self.mass == other.mass and
self.length == other.length and
self.time == other.time and
self.temperature == other.temperature and
self.amount == other.amount)
def is_dimensionless(self) -> bool:
return self == Dimension()
# Common physical dimensions
ENERGY = Dimension(mass=1, length=2, time=-2) # kg*m^2/s^2
FORCE = Dimension(mass=1, length=1, time=-2) # kg*m/s^2
VELOCITY = Dimension(length=1, time=-1) # m/s
PRESSURE = Dimension(mass=1, length=-1, time=-2) # kg/(m*s^2)
GAS_CONSTANT_DIM = ENERGY / Dimension(temperature=1, amount=1) # J/(mol*K)
def check_dimensional_consistency(
lhs_dim: Dimension,
rhs_dim: Dimension,
equation_label: str = ""
) -> dict:
"""Check whether both sides of an equation have the same dimensions."""
consistent = lhs_dim == rhs_dim
return {
"consistent": consistent,
"equation": equation_label,
"lhs_dimensions": lhs_dim,
"rhs_dimensions": rhs_dim,
"error": None if consistent else
f"Dimensional mismatch in {equation_label}"
}
# Example: verify Delta_G = RT ln(Kd)
# LHS: Delta G has dimensions of energy per mole
lhs = ENERGY / Dimension(amount=1) # J/mol
# RHS: R * T * ln(Kd)
# R has dimensions J/(mol*K), T has dimensions K, ln(Kd) is dimensionless
rhs = GAS_CONSTANT_DIM * Dimension(temperature=1) * Dimension() # J/mol
result = check_dimensional_consistency(lhs, rhs, "Delta_G = RT ln(Kd)")
print(f"Dimensionally consistent: {result['consistent']}")
Checkpoint
So far in this extension section: the pipeline's core four stages (generate, score, verify, report) handle mathematical derivations; dimensional analysis adds a lightweight physics-specific check that catches unit mismatches without invoking the full Lean theorem prover. Next, we address a different failure mode: computations that are mathematically correct but numerically unreliable.
Dimensional consistency catches unit mismatches, but a derivation can pass that test and still produce catastrophic results when executed on a computer.
Numerical Stability Verification
For computational derivations, a step may be mathematically correct but numerically unstable. Subtracting two nearly equal large numbers, dividing by a quantity near zero, or computing exponentials of large arguments are red flags. The pipeline can include a numerical stability checker that evaluates each step against known instability patterns:
def check_numerical_stability(step_text: str) -> dict:
"""Flag potential numerical stability issues in a computation step.
Checks for known patterns that cause floating-point problems.
"""
warnings = []
# Check for catastrophic cancellation
if re.search(r'\b(\w+)\s*-\s*\1\b', step_text):
warnings.append("Potential catastrophic cancellation: "
"subtracting similar quantities")
# Check for large exponentials
exp_match = re.search(r'exp\s*\(\s*(\d+)', step_text)
if exp_match and int(exp_match.group(1)) > 500:
warnings.append(f"Large exponential argument ({exp_match.group(1)}): "
"risk of overflow")
# Check for division by potentially small quantities
if re.search(r'/\s*\(?.*(?:epsilon|1e-|0\.0+[1-9])', step_text, re.IGNORECASE):
warnings.append("Division by potentially small quantity: "
"risk of numerical instability")
# Check for loss of significance in summation
if re.search(r'sum|Σ|sigma', step_text, re.IGNORECASE):
if re.search(r'alternating|(-1)\^', step_text):
warnings.append("Alternating series summation: "
"consider Kahan summation (a compensated summation "
"algorithm that tracks accumulated rounding error in a "
"separate variable) for numerical stability")
return {
"stable": len(warnings) == 0,
"warnings": warnings
}
The pipeline in this section verifies individual derivation steps. The next frontier is verifying entire discovery workflows: chains of reasoning that span hypothesis generation, experimental design, data analysis, and conclusion drawing. DeepMind's AlphaProof system (2024) demonstrated that LLM-guided formal verification can solve International Mathematical Olympiad problems; combined with AlphaGeometry 2, the system achieved a score equivalent to a gold medal at IMO 2024 (circa 2024), using a reinforcement learning loop where a language model proposes proof steps and Lean 4 provides ground-truth feedback. AlphaProof's key insight is that the language model and the formal verifier can train each other: the model learns which proof strategies succeed, and failed verification attempts generate targeted training data. Independently, the LEGO-Prover system (Xin et al., 2024) showed that LLMs can build libraries of reusable verified lemmas, growing a formal knowledge base that accelerates future proofs. Combined with the causal reasoning frameworks from Chapter 31: Causal Discovery and Causal Inference and the claim validation systems from Chapter 41: Scientific Claim Validation, this points toward discovery systems that produce not just results but machine-verifiable certificates of reasoning quality. The Discovery Workbench (Chapter 6) is designed to accommodate this verification layer as it matures.
8. Putting It Together: A Complete Worked Example
Let us trace the pipeline through a concrete problem from start to finish. The problem: find the minimum of \(f(x) = x + \frac{4}{x}\) for \(x > 0\).
Stage-by-Stage Trace
Stage 1 (Generate): The pipeline generates 4 candidate solutions. Candidate 1 uses calculus (take derivative, set to zero). Candidate 2 uses the arithmetic mean-geometric mean (AM-GM) inequality. Candidate 3 uses calculus but makes a sign error. Candidate 4 uses a numerical approach (evaluate at many points).
Stage 2 (Score): The PRM scores each step. Candidate 1: all steps score above 0.9 except the second derivative test (0.87). Candidate 2: all steps score above 0.92 (the AM-GM approach is cleaner). Candidate 3: step 2 scores 0.4 (the derivative is wrong). Candidate 4: step 1 scores 0.7 (numerical approach is valid but not rigorous). The ranker selects Candidate 2 (highest minimum score).
Stage 3 (Verify): The pipeline attempts to formalize Candidate 2's key step, the AM-GM inequality application. In Lean 4:
-- Lean 4: AM-GM for x + 4/x
-- For x > 0, by AM-GM: x + 4/x >= 2 * sqrt(x * 4/x) = 2 * sqrt(4) = 4
-- Equality holds when x = 4/x, i.e., x = 2
theorem am_gm_application (x : Real) (hx : x > 0) :
x + 4 / x >= 4 := by
have h4x : 4 / x > 0 := div_pos (by norm_num) hx
-- Use the fact that (sqrt(x) - sqrt(4/x))^2 >= 0
nlinarith [sq_nonneg (Real.sqrt x - Real.sqrt (4 / x)),
Real.sq_sqrt (le_of_lt hx),
Real.sq_sqrt (le_of_lt h4x),
Real.sqrt_mul_self (le_of_lt hx)]
nlinarith, a Lean tactic that decides nonlinear arithmetic goals by searching for a certificate of non-negativity from the provided hypotheses.Stage 4 (Report): The report confirms that Lean formally verified 3 of 4 steps (the AM-GM application, the equality condition, and the minimum value computation). The PRM scored the remaining step (problem setup) at 0.95; it is purely expository and was not sent to Lean. Overall confidence: "prm_high," because all mathematical content is either formally verified or high-confidence PRM-scored.
With the pipeline's architecture and output format established, the natural next question is how to reduce the orchestration overhead of wiring these four stages together.
The pipeline above has four explicit stages with manual data passing between them. DSPy (Khattab et al., 2023) provides a declarative framework for composing LLM-based modules into pipelines, reducing the orchestration code from ~200 lines to approximately 50 (as of 2025, DSPy 2.x has substantially reworked its API with typed predictors and a more Pythonic interface; consult the current documentation for updated module signatures). Each stage becomes a DSPy Module with typed signatures; DSPy handles prompt optimization, retry logic, and output parsing. For the verification pipeline, DSPy's ChainOfThought module replaces our manual CoT prompting, its Predict module replaces the PRM scoring calls, and a custom LeanVerify module wraps the subprocess interaction. The architectural pattern (generate, score, verify, report) remains identical.
import dspy
# DSPy reduces pipeline orchestration to module composition
class GenerateSolution(dspy.Module):
"""DSPy module for step-by-step solution generation."""
solve = dspy.ChainOfThought("problem -> solution")
class ScoreSteps(dspy.Module):
"""DSPy module for PRM-style step scoring."""
evaluate = dspy.Predict("problem, step, context -> score: float")
# Pipeline = GenerateSolution >> ScoreSteps >> LeanVerify >> Report
>> operator composes modules into a pipeline where outputs flow automatically between stages.Try It: Build a Lightweight Score-and-Verify Pipeline
You can build a simplified version of this section's pipeline using only the Anthropic SDK and Python's standard library (no Lean 4 installation required). This project replaces the formal verification stage with a secondary LLM cross-check, giving you the architectural pattern without the theorem prover dependency.
1. Define the problem and generate candidates. Pick a simple optimization problem (e.g., minimize \(f(x) = x^2 + 9/x\) for \(x > 0\)). Using the Anthropic API with claude-sonnet-4-20250514, generate three candidate solutions by calling the model three times with the same prompt but different budget_tokens values (8000, 10000, 12000).
2. Split and score each chain. Write a split_into_steps function using regex to break each candidate into numbered steps. For each step, call the model with the PRM prompt from this section (providing the problem, preceding steps, and current step) and parse the returned JSON score.
3. Rank and select the best chain. Compute the minimum PRM score across steps for each candidate. Select the candidate with the highest minimum score. Print a table showing each step's text preview and score.
4. Cross-verify low-scoring steps. For any step scoring below 0.85, call the model a second time with a different prompt: "Is this step mathematically correct? If not, what is the error?" Compare the cross-check verdict with the original PRM score. Flag steps where the two assessments disagree.
5. Generate the report. Print a structured summary: total candidates, number of steps, number cross-verified, number flagged, and an overall confidence label ("high" if all steps scored above 0.85, "medium" if cross-checks confirmed low-scoring steps, "low" if disagreements remain). Compare your pipeline's output against manually solving the problem to check whether the selected answer is correct.
The pipeline produces three confidence levels: "formally_verified" (every step checked by Lean), "prm_high" (all steps above threshold, some formally verified), and "prm_low" (at least one step below threshold and not formally verified). In practice, most scientific derivations land in "prm_high": the core mathematical steps verify, but expository framing does not (because it is not worth formalizing "we seek to minimize f"). A colleague once suggested a fourth level: "prm_suspicious," for derivations where the PRM gives a suspiciously uniform 0.95 to every step, suggesting the evaluator is not actually discriminating. We did not implement it, but the point stands: meta-evaluation of the evaluator is its own research problem.
Step-Through: PRM Scoring and Verification Routing
Trace through the scoring and verification routing logic with a tiny 4-step chain and a PRM threshold of 0.85.
Input chain (4 steps): Step A (setup), Step B (derivative), Step C (solve for critical point), Step D (second derivative test).
PRM scoring pass: Step A scores 0.96, Step B scores 0.72, Step C scores 0.91, Step D scores 0.83. The chain's minimum score is min(0.96, 0.72, 0.91, 0.83) = 0.72. The product score is 0.96 * 0.72 * 0.91 * 0.83 = 0.521: even when no single step looks disastrous, the cumulative confidence across four "decent" steps drops below 53%.
Verification routing (threshold = 0.85): Step A (0.96 >= 0.85): skip Lean. Step B (0.72 < 0.85): send to Lean, attempt formalization (up to 3 tries). Step C (0.91 >= 0.85): skip Lean. Step D (0.83 < 0.85): send to Lean, attempt formalization.
Lean results: Step B verifies on attempt 2 (lean_verified = True). Step D fails all 3 attempts (lean_verified = False).
Confidence calculation: formally_verified count = 1 (Step B). High-PRM steps contribute their scores: 0.96 + 0.91 = 1.87. Total confidence = (1 + 1.87) / 4 = 0.7175. Overall label: "prm_low" (Step D scored below threshold and was not formally verified). The pipeline exposed exactly one unverified weak step for human review.
Real-World Application: Semiconductor Design Rule Verification
Semiconductor manufacturers have explored variants of this generate-score-verify pipeline to check lithographic design rule derivations in chip manufacturing. Engineers specify constraints (minimum wire spacing, maximum current density) as optimization problems; the pipeline generates algebraic derivations, PRM-scores each step for physical plausibility, and routes critical inequalities to a satisfiability modulo theories (SMT) solver (Z3, a tool that automatically determines whether mathematical formulas involving arithmetic, inequalities, and logical constraints have satisfying assignments) for formal verification. Steps involving thermal expansion coefficients and process variation tolerances receive the heaviest scrutiny because errors in these steps have led to costly silicon re-spins in the past.
Exercise 29.4.1
Suppose the PRM assigns the following scores to a 5-step reasoning chain: [0.93, 0.88, 0.61, 0.90, 0.87]. Using a threshold of 0.85, (a) which steps would be sent to the formal verifier? (b) If the formal verifier confirms step 3 but rejects step 5, what overall confidence label would the pipeline assign ("formally_verified", "prm_high", or "prm_low")? (c) Compute the verification_confidence score using the formula from the code: formally verified steps count as 1.0 each, and high-PRM steps contribute their raw PRM score.
Hint
Steps below threshold: any step with score < 0.85 goes to Lean. That gives you steps 3 (0.61) and 5 (0.87 is >= 0.85, so it does NOT go to Lean). Re-read the threshold comparison carefully: the condition isstep.prm_score < prm_threshold, which is strict less-than. For the confidence label, check whether any step that scored below 0.85 failed formal verification.Lab: Measure How PRM Threshold Affects Verification Cost and Error Detection
Goal: Empirically determine the optimal PRM threshold for the verified reasoning pipeline by sweeping threshold values and measuring the tradeoff between verification cost (number of Lean calls) and error detection rate.
Tools needed: Python 3.10+, the Anthropic SDK (pip install anthropic), and optionally Lean 4 with Mathlib (you can substitute the Lean verification step with a second LLM cross-check call if Lean is not installed).
Setup (15 min): Copy the pipeline code from this section into a script. Define 5 test problems of varying difficulty: (1) minimize \(x^2 + 1\), (2) minimize \(x + 4/x\) for \(x > 0\), (3) minimize \(x^2 + y^2\) subject to \(x + y = 10\), (4) minimize \(x^2 + y^2 + 2/(xy)\) for \(x, y > 0\), (5) find the maximum area rectangle with perimeter 20. For each problem, generate 4 candidate chains and score them.
What to vary: Run the verification routing logic with thresholds 0.70, 0.80, 0.85, 0.90, 0.95. For each threshold, record: (a) how many steps are routed to verification, (b) how many pass verification, (c) total API calls made, (d) the overall confidence label.
What to observe: Plot threshold vs. number of verification attempts and threshold vs. confidence label distribution. Identify the "knee" where lowering the threshold further adds many verification calls but catches few additional errors. Compare this empirical knee against the default 0.85 threshold used in the section.
Exercises
- (Conceptual) The pipeline uses a PRM threshold of 0.85 to decide which steps to formally verify. Discuss the tradeoffs of setting this threshold higher (0.95) versus lower (0.7). How does the threshold affect: (a) the number of Lean compilations, (b) the false negative rate (errors missed), and (c) the total pipeline runtime? Propose an adaptive strategy that adjusts the threshold based on the problem's difficulty.
- (Coding) Implement the dimensional analysis checker for a complete physics derivation: the escape velocity formula \(v = \sqrt{2GM/R}\). Define the dimensions of each quantity (\(G\), \(M\), \(R\), \(v\)), compute the dimensions of the right-hand side, and verify they match the left-hand side. Then extend the pipeline to include dimensional checking as a lightweight pre-filter before Lean verification.
- (Analysis) Run the complete pipeline on three problems of increasing difficulty: (a) minimize \(f(x) = x^2 + 1\) for \(x \in \mathbb{R}\), (b) minimize \(f(x) = x + 4/x\) for \(x > 0\), (c) minimize \(f(x, y) = x^2 + y^2 + 2/(xy)\) for \(x, y > 0\). For each, record the number of candidates generated, steps scored, steps formally verified, and the overall confidence level. How does problem difficulty affect the pipeline's ability to formally verify steps? At what complexity does formal verification become the bottleneck?