LLM Tuning Patterns
Evidence-based patterns for configuring LLM parameters, based on APOLLO and Godel-Prover research.
Pattern
Different tasks require different LLM configurations. Use these evidence-based settings.
Theorem Proving / Formal Reasoning
Based on APOLLO parity analysis:
Parameter Value Rationale
max_tokens 4096 Proofs need space for chain-of-thought
temperature 0.6 Higher creativity for tactic exploration
top_p 0.95 Allow diverse proof paths
Proof Plan Prompt
Always request a proof plan before tactics:
Given the theorem to prove: [theorem statement]
First, write a high-level proof plan explaining your approach. Then, suggest Lean 4 tactics to implement each step.
The proof plan (chain-of-thought) significantly improves tactic quality.
Parallel Sampling
For hard proofs, use parallel sampling:
-
Generate N=8-32 candidate proof attempts
-
Use best-of-N selection
-
Each sample at temperature 0.6-0.8
Code Generation
Parameter Value Rationale
max_tokens 2048 Sufficient for most functions
temperature 0.2-0.4 Prefer deterministic output
Creative / Exploration Tasks
Parameter Value Rationale
max_tokens 4096 Space for exploration
temperature 0.8-1.0 Maximum creativity
Anti-Patterns
-
Too low tokens for proofs: 512 tokens truncates chain-of-thought
-
Too low temperature for proofs: 0.2 misses creative tactic paths
-
No proof plan: Jumping to tactics without planning reduces success rate
Source Sessions
-
This session: APOLLO parity - increased max_tokens 512->4096, temp 0.2->0.6
-
This session: Added proof plan prompt for chain-of-thought before tactics