# Higher-Order Theorem Proving on Complex corpus (val)

Source: [Higher-Order Theorem Proving on Complex corpus (val)](<https://www.sota2.com/research/sota/higher-order-theorem-proving-on-complex-corpus-val>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2026-02-26T05:59:01.739Z

Evaluation of model performance on higher-order theorem proving tasks using the validation split of the Complex corpus.

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

| Scope | Recorded value |
| --- | --- |
| Task | Higher-Order Theorem Proving |
| Dataset (including any stated split) | Complex corpus (val) |
| Metric | Proof Success |
| Unit | PERCENT |
| Direction | Higher is better |
| Results loaded | 8 of 8 |
| Coverage | All results currently returned for this benchmark |

Evaluation settings may differ between results. The original papers and recorded configurations are needed to establish comparability. A shared metric name alone does not establish an identical protocol.

## Metrics

- [Proof Success](<https://www.sota2.com/research/sota/higher-order-theorem-proving-on-complex-corpus-val.md?metric=Proof%20Success>): Higher is better; unit: PERCENT.

## Recorded results

| Method | Proof Success | Result date | Report paper |
| --- | --- | --- | --- |
| Loop tactic dependent | 38.9 | Not recorded | 68fa669b1e209131cea11574 |
| Trained on loop output | 36.8 | Not recorded | 68fa669b1e209131cea11574 |
| Loop | 36.3 | Not recorded | 68fa669b1e209131cea11574 |
| Deeper WaveNet | 32.65 | Not recorded | 68fa669b1e209131cea11574 |
| WaveNet | 31.72 | Not recorded | 68fa669b1e209131cea11574 |
| Wider WaveNet | 27.6 | Not recorded | 68fa669b1e209131cea11574 |
| ASM\_MESON\_TAC + argument selection | 9.2 | Not recorded | 68fa669b1e209131cea11574 |
| ASM\_MESON\_TAC | 6.1 | Not recorded | 68fa669b1e209131cea11574 |

### Loop tactic dependent

Proof Success: 38.9. Result ID: 698cfbba8b517eb4331e27db.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Training":"Reinforcement Learning","Argument selection":"Tactic dependent"}. This record does not assert independent reproduction.

### Trained on loop output

Proof Success: 36.8. Result ID: 698cfbba8b517eb4331e27da.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Training":"Supervised on reinforcement learning loop output"}. This record does not assert independent reproduction.

### Loop

Proof Success: 36.3. Result ID: 698cfbba8b517eb4331e27d9.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Training":"Reinforcement Learning","Argument selection":"Tactic independent"}. This record does not assert independent reproduction.

### Deeper WaveNet

Proof Success: 32.65. Result ID: 698cfbba8b517eb4331e27d7.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Training":"Supervised on human proofs","Blocks":4,"Layers per block":5}. This record does not assert independent reproduction.

### WaveNet

Proof Success: 31.72. Result ID: 698cfbba8b517eb4331e27d6.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Training":"Supervised on human proofs","Filters":128,"Blocks":2}. This record does not assert independent reproduction.

### Wider WaveNet

Proof Success: 27.6. Result ID: 698cfbba8b517eb4331e27d8.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Training":"Supervised on human proofs","Filters":256}. This record does not assert independent reproduction.

### ASM\_MESON\_TAC + argument selection

Proof Success: 9.2. Result ID: 698cfbba8b517eb4331e27d5.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

[Implementation](<http://deephol.org/>)

Recorded evaluation configuration: {"Description":"Baseline prover with argument list predicted by WaveNet"}. This record does not assert independent reproduction.

### ASM\_MESON\_TAC

Proof Success: 6.1. Result ID: 698cfbba8b517eb4331e27d4.

[Reporting paper](<https://www.sota2.com/research/paper/68fa669b1e209131cea11574.md>)

Recorded evaluation configuration: {"Description":"HOL Light built-in first order theorem prover baseline"}. This record does not assert independent reproduction.

Page 1 of 1. This is an index page, not the full collection.