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