automated-entropy-inequality-proving

Imported from hiyenwong/ai_collection (collection/skills/physics-math/automated-entropy-inequality-proving/SKILL.md). Install upstream with npx skills add hiyenwong/ai_collection --skill automated-entropy-inequality-proving. Copyright stays with the author.

Context

Shannon-type entropy inequalities are fundamental results in information theory that govern the relationships between entropies, mutual informations, and conditional entropies of random variables. Traditionally, proving these inequalities requires manual mathematical derivation using techniques like the polymatroid characterization of entropy regions. This methodology automates the process using fine-tuned language models combined with guided tree search, enabling discovery and verification of information-theoretic results at scale.

Core Methodology

1. Problem Formulation

• Represent the entropy inequality as a linear constraint on the entropy vector h = (H(X_S)) for all subsets S of variables
• Shannon-type inequalities are those derivable from basic inequalities:
  • Non-negativity: H(X) ≥ 0
  • Submodularity: I(X;Y|Z) ≥ 0 (equivalently, H(X|Z) + H(Y|Z) ≥ H(X,Y|Z))
• The goal: prove that a given linear combination of entropies is always non-negative

2. LLM-Guided Proof Step Generation

• Fine-tune a language model on a corpus of information theory proofs
• The LLM generates candidate proof steps:
  • Application of basic Shannon inequalities
  • Variable substitutions and marginalizations
  • Chain rule expansions and decompositions
• Each step transforms the target inequality into a simpler form

3. Guided Tree Search

• Tree structure: Root = target inequality, leaves = proven or disproven states
• Branching: At each node, the LLM proposes multiple candidate proof steps
• Guidance heuristic: Use a value function to rank branches:
  • Prefer steps that reduce the number of variables or terms
  • Prefer steps that align with known proof patterns
  • Penalize steps that increase complexity
• Search strategy: Beam search or A* with the value function as heuristic

4. Verification Engine

• Each proposed proof step is verified by a symbolic computation engine:
  • Check that the step follows from valid information-theoretic identities
  • Verify that all intermediate expressions are well-defined
  • Confirm that the final result implies the target inequality
• Only verified steps are accepted into the proof tree

5. Counterexample Search

• If no proof is found within the search budget:
  • Attempt to find a counterexample by constructing a joint distribution
  • Use the polymatroid characterization: check if the inequality holds for all points in the polymatroid
  • Report either a proof or a counterexample with the violating distribution

Implementation Steps

1. Parse the inequality: Extract the linear combination of entropies and conditional entropies
2. Initialize search tree: Root node with the target inequality
3. Generate candidates: Use the fine-tuned LLM to propose proof steps at the current node
4. Score and select: Apply the value function to rank candidates, select top-k for expansion
5. Verify steps: Use the symbolic engine to validate each selected step
6. Expand tree: Add verified steps as child nodes
7. Check termination: If a leaf node reaches a trivially true inequality (e.g., 0 ≥ 0), the proof is complete
8. Output: Return the proof tree (sequence of verified steps) or report failure with counterexample attempt

Pitfalls

• Non-Shannon inequalities: This method only proves Shannon-type inequalities (those derivable from basic submodularity). It cannot prove non-Shannon inequalities (e.g., Zhang-Yeung inequality) which require additional constraints beyond submodularity.
• LLM hallucination: The LLM may propose invalid proof steps. The verification engine is critical — never trust LLM output without symbolic validation.
• Search explosion: The proof tree can grow exponentially. Use aggressive pruning: discard branches that increase complexity beyond a threshold, or that revisit previously explored states.
• Numerical precision: When checking counterexamples via linear programming on the polymatroid, numerical precision issues can lead to false negatives. Use exact rational arithmetic when possible.
• Variable explosion: For n variables, the entropy vector has 2^n - 1 components. The search space grows rapidly with n. Limit to small numbers of variables (n ≤ 6) for practical use.

Verification

• Verify each proof step independently using symbolic algebra
• Confirm the proof chain: each step must follow logically from the previous
• For counterexamples: verify the violating distribution satisfies all basic Shannon inequalities but violates the target
• Cross-validate with known results: test on benchmark inequalities (e.g., data processing inequality, chain rule) where the expected result is known

Activation

entropy inequality proving, Shannon inequality automated, LLM theorem proving, guided tree search information theory, 熵不等式自动证明, automated information theory, proof search