llm-tuning-patterns

# 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