In January 2026, Logical Intelligence announced they had built the world's first commercial Energy-Based Reasoning Model (EBRM). The system, they claimed, could reason about formal constraints in ways that large language models fundamentally cannot. Turing Award winner Yann LeCun joined their leadership. Their Aleph system scored 99.4% on PutnamBench, the hardest formal mathematics benchmark. They positioned energy-based reasoning as the next paradigm beyond LLMs.
The core claim is compelling: instead of predicting the most likely next token, energy-based models learn to score what is valid. They assign low energy to correct reasoning traces and high energy to broken ones. In theory, this lets them evaluate partial proofs, localize failures, and guide search through proof space more intelligently than an autoregressive model ever could.
But do these claims hold up in practice?
We spent six weeks building our own EBRM system from scratch and testing it head-to-head against an LLM on formal theorem proving in Lean 4. The results are more nuanced than either side of the debate would suggest.
All experiments were run on a single M3 Max MacBook Pro.
Table of Contents
- The Experiment
- What We Built
- The Test
- Results: Three Conditions
- Condition A: EBRM Alone
- Condition B: LLM Alone
- Condition C: EBRM Guiding the LLM
- Does Scaling the EBRM Help?
- The Union: Complementary Value
- What About Logical Intelligence's Results?
- What We Learned
- Code
The Experiment
What We Built
We implemented a complete energy-based reasoning system for Lean 4 theorem proving. The system has three components:
1. Energy Model (EBRM). A Transformer encoder (6 layers, 384 dimensions, 13.3M parameters) maps proof states to a 192-dimensional latent space. A multi-head energy function scores how "correct" a proof transition looks. Low energy = the tactic likely advances the proof correctly.
The encoder learns two representations: z_goal = encode("{goal} [TAC] {tactic}") and z_state = encode("{state_before} [SEP] {state_after}"). The energy function scores the compatibility between goal-tactic pairs and state transitions. Training uses a contrastive ranking loss. For each proof step, the correct tactic-transition pair should receive lower energy than hard negatives sampled from the same theorem.
2. Langevin Proof Search. Instead of generating tactics token-by-token, we search for good proof steps by running Langevin dynamics in the encoder's latent space. Starting from the current proof state's encoding, we follow the energy gradient to find low-energy regions, then retrieve the nearest known tactics from a 50K-entry index.
We also use parallel tempering (replica exchange Monte Carlo) with 4 temperature chains to avoid getting stuck in local minima. This technique is borrowed from computational physics.
3. LLM Baseline. For comparison, we fine-tuned Qwen2.5-Coder-0.5B-Instruct with LoRA (2.9M trainable parameters) on 196K proof steps from the same training data. This gives the LLM the ability to generate specific Mathlib tactic applications.
The Test
We evaluated on the LeanDojo Benchmark 4 random test split: 718 testable theorems from Lean 4's Mathlib library. Each theorem gets a 120-second timeout with beam search (width 8, max depth 5). Same test set, same timeout, same beam parameters for every condition.
Why this benchmark? LeanDojo is the standard evaluation for neural theorem provers. The theorems range from simple lemmas (simp solves them) to multi-step proofs requiring chains of 3-5 tactics. It tests whether models can handle real-world mathematical reasoning, not toy problems.
Results: Three Conditions
Condition A: EBRM Alone
First, the purest test: can the energy model prove theorems without any LLM?
The EBRM-only system uses Langevin dynamics to search the latent space, retrieves candidate tactics from a 50K-entry nearest-neighbor index, and generates additional candidates via a custom Transformer decoder (25.7M params) conditioned on the latent vectors. No language model involved.
The result: 190/718 theorems proved (26.5%) with 39M total parameters, including 16 multi-step proofs and 2.9M total tactic attempts. The top tactics were simp (101), aesop (63), and intro (14).
The EBRM system proves 190 theorems on its own. That's 93% of the LLM's performance with 12.7x fewer parameters. Not bad, but not better.
Condition B: LLM Alone
The control: Qwen2.5-Coder-0.5B with simple beam search, no energy guidance.
The LLM proves 204/718 (28.4%) with 494M parameters, finding 30 multi-step proofs in 944K tactic attempts. Top tactics: simp (132), aesop (61), intro (50).
The LLM solves 14 more theorems than the EBRM and finds nearly twice as many multi-step proofs (30 vs 16). It also uses 3x fewer tactic attempts. Autoregressive generation is more sample-efficient than retrieval from Langevin search.
Condition C: EBRM Guiding the LLM
This is the critical test of the EBRM-as-search-guide hypothesis. Qwen generates candidate tactics, but the energy model scores each resulting proof state to guide beam search toward low-energy (promising) branches.
The result: 193/718 (26.9%) with 507M combined parameters, 20 multi-step proofs, 736K attempts.
The energy model makes the LLM worse. Condition C (193) solves 11 fewer theorems than the LLM alone (204). The energy function is over-pruning: it assigns high energy to proof states that are actually productive, causing beam search to abandon promising branches.
One silver lining: on the multi-step proofs that both methods solve, energy-guided search is 2.8x more efficient (505 attempts vs 1,397). The energy model is good at focusing search when it's already on the right track. It's bad at knowing which tracks are right in the first place.
We also tried expert iteration, fine-tuning the energy model on successful multi-step proof transitions. This recovered most of the gap (202/718, 28.1%) but still couldn't beat the unguided LLM.
Does Scaling the EBRM Help?
One possible objection: maybe 13.3M parameters isn't enough. Our initial EBRM encoder was only 2.7% the size of Qwen (494M). Perhaps with more capacity, the energy model would shine.
So we scaled up to a 95M-parameter encoder (12 layers, 768 dimensions, 384 latent dimensions) trained on all 237K training examples (5x more data). This larger model is measurably better at energy discrimination. Picking the correct tactic from 10 candidates improves from 24.3% to 26.7% Rank@1 accuracy.
But does it prove more theorems?
No. Despite 7x more parameters and 5x more data, the larger EBRM performs identically on actual theorem proving. Better energy discrimination doesn't translate to more theorems proved. The EBRM approach appears to hit a ceiling around 26% regardless of scale.
The Union: Complementary Value
If the EBRM can't beat the LLM, can it at least find theorems the LLM misses? We computed the union of all methods:
Yes. The EBRM finds 7 theorems that Qwen alone cannot solve. For example, Nat.lcm_comm was found through Langevin retrieval, Subgroup.Normal.comap through multi-step beam search at depth 3, and uniformity_le_symm via latent space search.
The union of all approaches solves 224/718 (31.2%), 20 more theorems than the best single method. The EBRM contributes genuine value as a diverse search strategy, not as a superior reasoning engine.
What About Logical Intelligence's Results?
Logical Intelligence's Aleph system scored 99.4% on PutnamBench (668/672 problems). Legitimately impressive. But there's a critical detail in their own blog post:
"Aleph uses reasoning models (currently standard LLMs) for three tasks"
The system that achieves 99.4% on PutnamBench uses GPT-5.2 as its reasoning engine, not their energy-based model Kona. Aleph is an orchestration layer. It breaks problems into subproblems, generates Lean proofs, and refines based on verification feedback. Good engineering, but the heavy lifting is done by an LLM.
Their energy-based model Kona is described as a future integration: "Integrated with Kona... it combines a purpose-built reasoning engine with a production-grade agent." The EBRM is positioned for constraint enforcement and validation, not proof generation.
Our experiments directly tested the core claim: can energy-based reasoning outperform autoregressive generation for theorem proving? At the scales we tested, the answer is no.
What We Can't Rule Out
Our experiments don't prove that EBRMs can never work for reasoning. There are important caveats:
- Scale: We tested up to 95M parameters. Logical Intelligence may be training at much larger scale with different architectures.
- Architecture: Our contrastive energy model is one design choice. Other energy function designs (diffusion-based, flow-based) might perform differently.
- Training objective: We used ranking loss on proof transitions. Other objectives (denoising, iterative refinement) are possible.
- Application domain: EBRMs might be more useful for constraint checking and verification than for proof generation. Scoring "is this proof step valid?" is different from "what proof step should I try next?"
- Hybrid architectures: An energy model trained at the same scale as the LLM (billions of parameters) with specialized architecture might behave differently.
What We Learned
1. Energy Discrimination ≠ Search Guidance
Our EBRM achieves 26.7% Rank@1 at picking the correct tactic from 10 candidates, well above the 10% random baseline. But this discrimination ability doesn't translate to useful beam search guidance. The energy function is good at ranking when given the right candidates. It's bad at steering search away from dead ends in the vast proof space.
This gap between discrimination and generation is something the energy-based reasoning community needs to address.
2. Retrieval is the EBRM's Real Strength
In Condition A, 90% of proofs came from the retrieval decoder, nearest-neighbor lookup in the energy model's latent space. The custom Transformer decoder and Langevin trajectory sampling contributed very little. The EBRM's real value is as a learned embedding space for tactic retrieval, not as an energy-based search algorithm.
3. Complementary > Superior
The best result isn't any single system. It's the union of diverse approaches. EBRM-only, LLM-only, and expert-iterated systems each find unique theorems. The path forward for theorem proving isn't choosing between paradigms. It's combining them.
4. The Marketing vs. Engineering Gap
Logical Intelligence's PutnamBench result is real engineering achievement, but it's achieved by GPT-5.2 + Lean verification + clever orchestration, not by energy-based reasoning. The gap between what's marketed ("AI Certainty," "beyond LLMs," "AGI") and what's demonstrated (a good LLM wrapper) is worth noting.
This doesn't mean their EBRM work is worthless. Constraint enforcement and formal verification are genuinely important applications. But claiming EBRMs are "beyond LLMs" for reasoning requires evidence of EBRMs actually outperforming LLMs at reasoning tasks. Neither they nor we have shown that.
Summary of Results
SOTA Context
Our systems are well below SOTA. ReProver uses premise retrieval from the full Mathlib corpus and 10-minute timeouts (vs our 2 minutes). Modern 7B+ provers are in a different league entirely. But our comparison between EBRM and LLM approaches is controlled and fair: same data, same timeout, same beam parameters.
Code
The full implementation (model architectures, training scripts, proof search experiments, and evaluation results) is available in our research repository. Access requires a subscription: github.com/latent-node/research