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: 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

llm-tuning-patterns