Towards Symbolic Generalization For Neural Reasoning

By Yuhuai Wu

What is reasoning？

Example 1: Theorem Proving

Color: union

Type: progression

Size: constant

Example 2: Raven’s Progressive Matrices

Example 3: Playing StarCraft

Reasoning

Symbolic Generalization

Generalization vs Symbolic Generalization

data distribution

training set

test set

training distribution

training set

test set

test� distribution

shared “rules”

Existing methods

​

• Unrobust to distribution shift.
• Extrapolation using interpolation.
• Very expensive. Unlikely to cover all cases.

How？

Thesis of the talk:

• Learning modular/symbolic representations.
• Boosted by planning.

Outline of the Talk

​

• Modularity learning.
• Scattering Compositional Learner.
• OPtions as REsponses (OPRE) agent.
• MCTS on INT dataset.
• General theorem proving
• A better symbolic representation: IsarStep Dataset.

The Scattering Compositional Learner: Discovering Objects, Attributes and Relationships for Analogical Reasoning [paper]

Roger Grosse

Jimmy Ba

Honghua Dong

Color: union

Type: progression

Size: constant

Example

Size: Progression

Color: Progression

Size: Constant

Color: Constant

Key observation: Composition!

​

​

​

Color

Progression

Constant

Size

Key Idea: represent each component with a NN

Size

Progression

Constant

Color

Key Idea: represent each component with a NN

Progression

Constant

Size

Color

Key Idea: represent each component with a NN

Progression

Constant

Progression

Constant

Size

Color

Key Idea: represent each component with a NN

Progression

Constant

Why?

​

• Progression/Constant neural network are encouraged to be compatible with both Color and size neural networks.

​

• Recognizing relationship (e.g., Progression) regardless of the type of attribute → generalizing to novel attributes.

The Full Architecture

Balanced-RAVEN

PGM

Interpretable Representation: Attribute

Interpretable Representation: Relationship

Generalization to novel analogies

Summary

• Introduce an architecture that learns to discover the underlying compositional structures:
• Extracting objects.
• Extract features for each object.
• Recognize relationship among features.

​

• Modular learning enables symbolic generalization.

​

Outline of the Talk

​

• Modularity.
• Scattering Compositional Learner.
• OPtions as REsponses (OPRE) agent.*
• MCTS on INT dataset.
• General Theorem Proving
• A better symbolic representation: IsarStep Dataset.

OPtions as REsponses �[paper]

Maria Eckstein

Remi Leblond

Sasha Vezhnevets

Joel Leibo

Motivation

• HRL for generalization.
• Learn a menu of behaviors.
• Respond with the right behavior.
• Generalize to novel problems.

​

beats

beats

beats

Motivation

• Natural options in Multi-Agent Reinforcement Learning.
• Options as Responses to different opponents.

beats

beats

beats

Running example

Running with Scissors:

• Purple = rock, cyan = paper, brown = scissors
• Players gather resources to control their commitment to a strategy (R/P/S)
• Partial observability

​

Problems = different opponent policies

Behaviours = pick R/P/S, attack, scout

Generalisation = novel opponents

​

• Zero-sum
• concealed information =

opponent observation and inventory

• non-transitive reward

OPtions as REsponses (OPRE) agent

Policy over options p(z|x_≤t )

Estimate of concealed info

Options 𝜂(a|z,x_≤t )

Response to concealed info

Picking paper!

Opponent has rock!

KL

q(z|x_t′)

x_t′

concealed

information

V_𝜋=∑_zq(z|x_t′)c(x_≤t ,z)

𝜋

x_t

p(z|x_≤t )

agent

observation

𝜇

𝜇 =∑_z p(z|x_≤t )𝜂(a|z,x_≤t )

𝜋 =∑_z q(z|x_t′) 𝜂(a|z,x_≤t )

Credit assignment

Measuring generalisation in MARL

Held out agents

(specialists trained with pseudo-rewards)

Self-play

(6 agents)

Generalisation curves

R P

​

S

R bot OPRE

Episode start

R bot collects R;

OPRE moves left

OPRE sees that all R is missing; evidence for R bot jumps up

OPRE travels to P area and picks up all P

OPRE searches for the bot and tags it

Time in episode

p(z)

Latent activations

Summary

• Options as Response framework in MARL, via two levels of credit assignment: 1. which strategy to use? 2. How well the strategy was executed.

​

• Interpretable options.

​

• Modular learning enables better generalization in RL.

​

Predefined Modular Structures

• In those two works, we have seen modular structures from learning.

​

• In the following two works of theorem proving, the (primitive) modular structures are given, as symbolic rules in theorem proving.

​

​

Outline of the Talk

​

• Modularity.
• Scattering Compositional Learner.
• OPtions as REsponses (OPRE) agent.
• MCTS on INT dataset.*
• General Theorem Proving
• A better symbolic representation: IsarStep Dataset.

INT: an INequality Theorem Proving Dataset for �Benchmarking Generalization [paper]

Roger Grosse

Jimmy Ba

Albert Jiang

Theorem proving challenge: Learning

​

• Learn to generalize to theorems unseen in training.
• An algorithm that overcomes distribution shift.

​

​

• Systematic benchmarks for evaluation.
• Our work: INT.

INT: An INequality Theorem Proving Dataset

​

• Inequality theorems.
• Various dimensions of generalizations.
• Proof interface mimics modern ITP.
• Lightweight, fast simulation.

​

Proof system

​

• Proof as graph manipulation

43

A proof in LEAN

A proof in our system

Generator : An simple example

​

1. Initial conditions: A = A, B=B, C=C

Axioms orders: (A.C., A.C.)

​

2. A+B = B+A

​

Apply additional_commutativity (A, B)

​

3. (A+B)+C = C+(A+B)

​

Apply additional_commutativity (A+B, C)

Substitute 2 to 3

​

4. (A+B)+C = C+(B+A)

​

Six Dimensions of Generalization

​

• Randomness in generator algorithm
• Varying initial premises
• Varying axiom combinations (AB),(BC) -> (AC)
• Varying axiom orders (ABC) -> (ACB)
• Number of unique axioms (K)
• Varying proof lengths (L)

45

Proof Lengths

46

Improving Generalization

​

• Planning helps generalize to new theorems?

Boosted by planning

48

Boosted by planning

49

Summary

• Introduce a dataset that allows benchmarking six dimensions of generalization.
• Randomness in generator algorithm
• Varying initial premises
• Varying axiom combinations
• Varying axiom orders
• Number of unique axioms (K)
• Varying proof lengths (L)

​

• Planning with symbolic actions greatly helps generalization.

Outline of the Talk

​

• Modularity.
• Scattering Compositional Learner.
• OPtions as REsponses (OPRE) agent.
• MCTS on INT dataset.
• General Theorem Proving
• A better symbolic representation: IsarStep Dataset.*

Modelling High-level Mathematical Reasoning �in Mechanised Declarative Proofs [paper]

Lei Yu

Laurence Paulson

Wenda Li

Declarative Proof vs. Tactic Proof

IsarStep Dataset

IsarStep Dataset

IsarStep Dataset Statistics

• We have mined the largest repository of mechanised proofs:
• Isabelle proof.
• 143K lemmas (increased by 10k annually).
• Combined with Isabelle library, we have in total 204K lemmas, compared to:
• 71K in CoqGym, 11K in HolStep, 29K in HolList, 1.6K in GamePad.
• Topics includes:
• Foundational logic, advanced analysis, computer algebra, cryptographics, data structures.
• 850K data points for IsarStep.

Training as a seq-2-seq task

Word Embeddings

Summary

• The largest theorem proving dataset.
• Use declarative proof style to do more efficient search and planning.
• More detailed examples of the agent performing multi-step reasoning found in the paper.

Outline of the Talk

​

• Modularity.
• Scattering Compositional Learner.
• OPtions as REsponses (OPRE) agent.
• Planning.
• MCTS on INT dataset.
• A better symbolic representation: IsarStep Dataset.*
• Application
• GNNs for branching heuristics with SharpSAT. *

Learning Branching Heuristics for Propositional Model Counting [paper]

Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris Maddison, Roger Grosse, Edward Lee, Sanjit Seshia, Fahiem Bacchus

​

by

Sharp SAT Solver

Use a learned heuristic!

Training

​

• Graph Neural Network for representing formulas.
• Evolution Strategy
• The exploration complexity of RL is a function of |A| and horizon, where as ES does not depend on both.

Generalizing to problem of much larger size

3 days (SharpSAT) vs. 9 hours (Learned)!!

Future directions

• There are many opportunities!
• Improve reasoning architectures for IsarStep.
• Learning to discover modular structures with predefined primitive structure. Macro theorems!
• Theoretical understanding of neural architectures for reasoning.

​