Twitch: Learning Abstractions for Equational Theorem Proving

This paper introduces Twitch, a tool that automatically discovers reusable term abstractions from failed or successful proofs to enhance the performance of the Twee equational theorem prover, resulting in the solution of new problems and significant speed-ups on existing benchmarks.

The Gist

Imagine you are trying to solve a massive, incredibly complex jigsaw puzzle. You have a box with billions of pieces, but you don't know what the final picture looks like. You have a robot assistant (the Theorem Prover) whose job is to find the right pieces and snap them together to solve the puzzle.

The problem? The robot is very fast, but it's also very "dumb." It tries to connect every piece to every other piece. It looks at billions of combinations, but most of them are useless. It gets overwhelmed, wastes time, and often gives up before finding the solution.

This is the story of Twitch, a new tool designed to teach a robot how to be smarter by learning from its own mistakes and successes.

The Core Idea: Learning to Recognize Patterns

In the world of math proofs, a "proof" is just a long chain of logical steps. Sometimes, in these chains, you see the same weird shapes or patterns over and over again.

• The Old Way: The robot just looks at the size of the pieces. Big pieces? Maybe ignore them. Small pieces? Maybe try them. It's a simple rule, but it misses the big picture.
• The Twitch Way: Twitch says, "Wait a minute! I've seen this specific shape before. It keeps showing up in the solutions to other puzzles. Let's give that shape a special 'VIP pass' so the robot notices it immediately."

These special shapes are called Abstractions. Think of them as shorthand notes or stickers that say, "This complicated thing is actually just one simple concept."

How Twitch Learns (The Two Modes)

Twitch has two ways to learn these patterns, kind of like how a student learns for a big exam:

1. The "Study Hall" Method (Domain Abstractions)

Imagine you are studying for a math test on Lattices (a specific type of math structure). Before you tackle the super-hard final exam question, you look at the solutions to the easier practice problems you've already solved.

• You notice that in almost every easy solution, there's a specific pattern of numbers that keeps appearing.
• Twitch takes all those easy solutions, finds the common patterns, and creates a "cheat sheet" of abstractions.
• When you finally face the hard exam question, you hand the robot this cheat sheet. The robot now knows, "Oh, I've seen this pattern before! It's important!" and solves the problem much faster.

2. The "Gritty Determination" Method (Partial Proof Abstractions)

Sometimes, you don't have any easy practice problems. You just have the hard one, and the robot tries to solve it but fails after running for a while.

• Instead of giving up, Twitch looks at the robot's failed attempt. It says, "Okay, you didn't finish, but look at all the steps you took. You kept building these specific structures before you got stuck."
• It extracts those structures, turns them into abstractions, and tells the robot: "Try again, but this time, pay extra attention to these specific shapes you were building."
• Often, this second attempt is successful because the robot finally focused on the right clues.

The Secret Weapon: "Stitch"

How does Twitch actually find these patterns? It uses a tool called Stitch.

Imagine you have a long, messy sentence:

"The cat sat on the mat, and the cat ran to the mat, and the cat slept on the mat."

Stitch looks at this and says, "Hey, 'the cat' and 'the mat' keep showing up. Let's invent a new word, 'C', for 'the cat' and 'M' for 'the mat'."
Now the sentence becomes:

"C sat on M, and C ran to M, and C slept on M."

It's shorter, cleaner, and easier to understand. In the math world, Stitch finds these "C" and "M" patterns in millions of lines of code and math proofs, compressing them into simple, reusable rules.

The Result: Faster and Smarter

The researchers tested Twitch on a huge library of math problems (called TPTP).

• Without Twitch: The robot would get stuck on 12 very hard problems, running for hours and giving up.
• With Twitch: The robot solved all 12 of those hard problems. In fact, for many problems, it solved them twice as fast.

Why This Matters

Think of the robot as a brilliant but naive detective. It has all the facts, but it doesn't know what clues are important.

• Old approach: The detective tries to interview every single person in the city.
• Twitch approach: Twitch acts like a seasoned mentor who whispers, "Don't talk to everyone. Just talk to the guy in the red hat; he's the key to the case."

By automatically learning these "red hats" (abstractions) from past cases, Twitch helps the robot solve problems that were previously impossible, making automated math reasoning much more powerful and efficient.

Technical Summary

Here is a detailed technical summary of the paper "Twitch: Learning Abstractions for Equational Theorem Proving."

1. Problem Statement

Automated theorem provers (ATPs), particularly saturation-based ones like Twee (an equational theorem prover), face a massive search space. They must navigate millions of potential inferences (critical pairs) to find a proof, relying on simple heuristics (like term size) to prioritize which inferences to pursue.

• The Challenge: Simple metrics often fail to identify "interesting" term shapes or clauses that are crucial for solving difficult problems.
• Current Limitations: While human-guided strategies (e.g., weighting, resonance, hints) exist to inject domain knowledge, they require manual effort. Automatically discovering these "interesting" term patterns without human intervention remains an open problem.
• Goal: To automatically discover abstractions (recurring term patterns) from proof attempts or related theorems and use them to guide the search process more effectively than simple size-based heuristics.

2. Methodology

The authors propose Twitch, a system that integrates the Stitch tool (originally designed for program synthesis) with the Twee theorem prover. The core idea is to treat proof terms as data to be compressed; the "compression" reveals the underlying abstractions.

A. The Core Mechanism: Stitch

• Input: A set of terms (extracted from proofs).
• Process: Stitch attempts to find a set of function definitions (abstractions) that maximally compress the input terms. It maximizes the product of the function definition size and the number of times it can be used.
• Output: Abstractions (e.g., defining $g(x) := f(x, x)$ to replace repeated occurrences of $f(x, x)$).
• Translation: Proof terms are translated into higher-order $\lambda$-terms for Stitch, then translated back to first-order logic if the resulting abstraction is first-order.

B. Two Modes of Abstraction Generation

Twitch operates in two distinct modes to generate abstractions:

1. Partial Proof Abstractions (Failure-Driven):

   • Scenario: Used when no related solved problems exist for a hard conjecture.
   • Process:
     1. Run Twee on the hard problem ($P_h$) for a fixed time.
     2. If it fails, extract the derived lemmas from the partial proof.
     3. Score lemmas based on "interestingness": $s(l=r) = \frac{|T(l=r)|}{|l=r|^2}$, where $|T|$ is the total size of the proof terms and $|l=r|$ is the size of the lemma. This favors simple statements with long proofs.
     4. Select the top $k$ lemmas, extract all terms, and run Stitch to find abstractions.
     5. Re-run Twee on $P_h$ using these abstractions.

2. Domain Abstractions (Curriculum Learning):

   • Scenario: Used when a domain contains both "easy" (solved) and "hard" (unsolved) problems.
   • Process:
     1. Solve "easy" problems in the domain using Twee.
     2. Extract terms from these successful proofs and run Stitch to generate local abstractions for each problem.
     3. Filter these local abstractions: only keep those that empirically speed up the proof of the specific problem they came from (measured by a speedup metric).
     4. Aggregate all "good" local abstractions and run Stitch again on this aggregate set to find common, higher-level domain abstractions.
     5. Apply these domain abstractions to the hard problems.

C. Integration with Twee

Instead of adding abstractions as new axioms (which expands the search space and can cause timeouts), Twitch modifies Twee's heuristic ranking function.

• Weighting Strategy: Twee ranks critical pairs based on a weight function $w(t)$.
• Modification: If a term matches an abstraction pattern $A$, its weight is reduced.
  • $w(A\sigma) = w_A + \sum w(x\sigma)$
  • This makes inferences involving these patterns "cheaper" and thus more likely to be selected, without altering the search space itself.

3. Key Contributions

1. Automated Abstraction Discovery: A novel method to automatically generate term abstractions from failed proof attempts and successful proofs of related theorems using the Stitch tool.
2. Curriculum Learning for ATPs: A methodology inspired by curriculum learning, where simpler problems in a domain are solved first to extract reusable structural patterns that guide the proof of harder problems.
3. Native Heuristic Integration: An implementation of abstractions directly into the Twee prover's heuristic function, avoiding the search space explosion associated with adding definitional axioms.
4. Empirical Validation: Comprehensive evaluation on the TPTP (Thousands of Problems for Theorem Provers) dataset, specifically focusing on Unit Equality (UEQ) problems.

4. Experimental Results

The system was evaluated on 1,041 unsatisfiable UEQ problems from TPTP v9.2.1 across nine domains (e.g., Group Theory, Lattice Theory).

• Solving Hard Problems:
  • Twitch enabled Twee to solve 12 rating-1 problems (problems rated as the most difficult, where 90% of ATPs fail).
  • In total, 18 hard problems (Rating $\ge$ 0.9) were solved within 1000 seconds using domain abstractions.
  • Case Study (LAT075-1): A problem regarding modular ortholattices. Without abstractions, Twee took ~250s. With domain abstractions (specifically $f(x,x)$ and others), it solved in ~32s.
• Runtime Improvements:
  • Domain Abstractions: When combined with Twee's "goal flattening" strategy, domain abstractions roughly halved the runtime for problems already solvable within 300 seconds and solved ~25 additional problems within the 300s limit.
  • Partial Proof Abstractions: Provided modest improvements and solved more problems after the 300s mark, though less effectively than domain abstractions.
• Abstractions vs. Axioms:
  • The paper compares using abstractions as heuristics (Twitch's approach) vs. definitional axioms.
  • Result: Using abstractions as heuristics is more robust. Adding many axioms often leads to timeouts due to search space explosion, whereas heuristic weighting allows for a larger pool of abstractions without significant slowdowns.

5. Significance and Future Work

• Significance:
  • Demonstrates that automatic compression of proof terms is a viable method for discovering search-guiding patterns, removing the need for manual human guidance.
  • Proves that "curriculum learning" (learning from easy problems to solve hard ones) is effective in equational theorem proving.
  • Offers a lightweight, interpretable alternative to statistical learning methods (like ENIGMA), as the abstractions are explicit syntactic patterns.
• Limitations & Future Directions:
  • Brittleness: The current implementation is sensitive to rewriting; if a term matching an abstraction is rewritten by another rule, the abstraction match is lost.
  • Domain Curation: The quality of domain abstractions depends on the similarity of the "easy" problems to the "hard" target.
  • Future Work: Refining the "interestingness" scoring of lemmas, exploring multi-objective optimization (proof length vs. speed), and potentially using Large Language Models (LLMs) to propose abstractions directly.

In conclusion, Twitch represents a significant step toward self-improving theorem provers that can learn structural patterns from their own search history and the history of related problems, significantly boosting performance on difficult equational reasoning tasks.