Skip to content

Commit bd37e09

Browse files
Jonathan D.A. Jewellclaude
andcommitted
feat: register Vampire in Julia ML and Chapel parallel layers
- Added VAMPIRE (Tier 5 FOL ATP) to Julia ProverType enum - Added Vampire to Chapel parallel dispatcher - Updated prover count from 12 to 14 (Vampire + Idris2) - Julia layer can now recommend Vampire for FOL problems - Chapel layer can dispatch Vampire across cluster nodes Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
1 parent 3d49e12 commit bd37e09

2 files changed

Lines changed: 11 additions & 5 deletions

File tree

chapel_poc/parallel_proof_search.chpl

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
use Time;
55
use Random;
66

7-
config const numProvers = 12;
7+
config const numProvers = 14;
88
config const verbose = true;
99

1010
// Proof result type
@@ -170,7 +170,8 @@ proc beamSearchProof(goal: string, initialProver: string, beamWidth: int = 5) {
170170
// Main demonstration
171171
proc main() {
172172
var provers = ["Coq", "Lean", "Isabelle", "Agda", "Z3", "CVC5",
173-
"ACL2", "PVS", "HOL4", "Metamath", "HOL Light", "Mizar"];
173+
"ACL2", "PVS", "HOL4", "Metamath", "HOL Light", "Mizar",
174+
"Vampire", "Idris2"];
174175

175176
var goal = "forall n m : nat, n + m = m + n";
176177

src/julia/EchidnaML.jl

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,14 @@
55
EchidnaML
66
77
ECHIDNA (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance)
8-
Machine Learning Module - Universal Neural Solver for 12 Theorem Provers
8+
Machine Learning Module - Universal Neural Solver for 14 Theorem Provers
99
1010
Generalizes ECHIDNA's universal neural architecture to support:
1111
- Tier 1 (6): Agda, Coq/Rocq, Lean, Isabelle, Z3, CVC5
1212
- Tier 2 (3): Metamath, HOL Light, Mizar
1313
- Tier 3 (2): PVS, ACL2
1414
- Tier 4 (1): HOL4
15+
- Tier 5 (2): Vampire (FOL ATP), Idris2
1516
1617
Architecture:
1718
- Graph Neural Networks for theorem embeddings
@@ -45,7 +46,7 @@ export encode_proof_state, decode_prediction
4546
export NeuralSolver, create_solver, train_solver!, predict_premises
4647
export start_api_server
4748

48-
# Prover enumeration - all 12 supported provers
49+
# Prover enumeration - all 14 supported provers
4950
@enum ProverType begin
5051
# Tier 1 - Primary targets (6)
5152
AGDA = 1
@@ -67,6 +68,10 @@ export start_api_server
6768

6869
# Tier 4 - Complex (1)
6970
HOL4 = 13
71+
72+
# Tier 5 - First-Order ATPs & Extended (2)
73+
VAMPIRE = 14 # First-order ATP
74+
IDRIS2 = 15 # Dependent types
7075
end
7176

7277
# Core data structures
@@ -198,7 +203,7 @@ function __init__()
198203
# Create checkpoint directory if it doesn't exist
199204
mkpath(CONFIG[].checkpoint_dir)
200205

201-
@info "EchidnaML initialized - Universal Neural Solver for 12 Theorem Provers"
206+
@info "EchidnaML initialized - Universal Neural Solver for 14 Theorem Provers"
202207
@info "Architecture: GNN + Transformer | Framework: Flux.jl | Device: $(CUDA.functional() ? "GPU" : "CPU")"
203208
end
204209

0 commit comments

Comments
 (0)