Primary evidence
- Thor: Wielding Hammers to Integrate Language Models and Automated Theorem ProversS1 · Primary research · Paper · 2022-05-22
Thor integrates language models with automated theorem-prover hammers
The framework uses theorem-prover hammers for premise selection while leaving other proof decisions to the language model.
What happened?
Thor increased a language model's success on the PISA dataset from 39% to 57% and matched leading miniF2F methods with less compute.
Why it matters
It highlighted a durable design principle: use symbolic tools where exhaustive reliability is strong and learned models where generation is needed.
Significance rationale: Thor was an early explicit neuro-symbolic architecture in which language models delegated premise-selection bottlenecks to classical automated provers.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- AI primary, human verified
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic, Hybrid
- AI contribution
- The language model generated proof actions while automated provers supplied premise-search assistance.
- Human contribution
- Researchers designed the integration protocol and evaluation across theorem-proving environments.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-11
Technical details
- Systems
- thor
- Organizations
- university-of-cambridge, microsoft-research
- Problems
- pisa, minif2f
- Methods
- hammer, premise-selection, language-model
Sources & artifacts
- Thor: Wielding Hammers to Integrate Language Models and Automated Theorem ProversS1 · Primary research · Paper · accessed 2026-09-10
Verification history
- 2022-05-22 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
Corrections
No corrections recorded.