Logical Intelligence

Further reading Formal verification (Wikipedia) · Automatic Formal Verification for Code Generation (Logical Intelligence) · Frequently Asked Questions on seL4 (seL4 Foundation) · I-JEPA: The first AI model based on Yann LeCun's vision for more human-like AI (Meta AI) · Proof assistant (Wikipedia) · Energy-Based Models for Reasoning, LLMs for the Interface (Logical Intelligence)

1. i.

   No universal checker

   There is a ceiling built into computer science. Rice's theorem says every non-trivial question about what a program does, such as whether it finishes on every input, is undecidableImpossible for any algorithm to answer correctly in every case.. No single tool can answer those questions for all programs. So verification tools either narrow the question or leanA proof assistant and programming language whose checker certifies that a proof is correct. on someone to supply the proof.

2. ii.

   Proofs outweigh code

   The best-known verified operating system kernel, seL4, started out at roughly 8,700 lines of C. Its proof ran to about 200,000 lines, and the proof base has since grown past a million. Writing the spec and most of the proof by hand is expensive enough that formal verification has only made sense in a few places, like core cloud infrastructure.

3. iii.

   One token at a time

   The obvious fix is to let a language model write the proofs. But language models generate text tokenA small chunk of text, often part of a word, that a language model reads and writes one at a time. by token, so revising an early step usually means regenerating everything after it. They are trained to predict the next token, which is not the same as getting a long chain of reasoning right from end to end. A proof is exactly such a chain.

Further reading Rice's theorem (Wikipedia) · seL4 explained, the 10,000-line kernel with a million lines of proof (Webiano) · Automatic Formal Verification for Code Generation (Logical Intelligence) · Energy-Based Models for Reasoning, LLMs for the Interface (Logical Intelligence)

Further reading Logical Intelligence's Aleph Solves PutnamBench (Logical Intelligence) · Automatic Formal Verification for Code Generation (Logical Intelligence)

1. Step 1: Score the whole attempt

   Kona, the company's energy-based reasoning model, puts a score on reasoning traces, including half-finished ones. That matters because a score on a partial trace can point at which step broke a constraint, rather than just reporting failure at the end. Kona also works on the whole trace at once, in a continuous latent spaceThe internal numerical space where a model represents problems, rather than as words., so it can nudge any part of it towards lower energy.

2. Step 2: Language at the edges

   Language models still have a job. They are good at turning fuzzy human requirements into rough formal structure and explaining failures. The bet is that the hard middle, keeping spec, code and proof consistent with each other, suits an energy model, whose learned energy acts as a cheap but imperfect verifier.

3. Step 3: Let Lean decide

   Aleph, the orchestration layer, coordinates calls to Kona, language models and other tools. Its proofs are written in Lean and certified by Lean's own deterministic checker, so a wrong answer can't sneak through. On PutnamBench, a set of 672 hard competition maths problems, Aleph generated proofs for 668.

Further reading Energy-Based Models for Reasoning, LLMs for the Interface (Logical Intelligence) · Automatic Formal Verification for Code Generation (Logical Intelligence) · Logical Intelligence's Aleph Solves PutnamBench (Logical Intelligence)

• Does the spec say what you meant?

  A proof shows the code matches its formal specification, not necessarily what a person intended. The more ambitious setups have AI write the spec too, starting from a plain-language description, which moves the question of intent rather than settling it.

• Who checks the checker?

  Proof checkers can be small, some with under a thousand lines of core code, which makes them checkable in turn. They are not flawless: a claimed disproof of the Collatz conjecture was announced as verified in Lean, then found to rely on a bug in Lean itself.

• How do you train an energy model well?

  In the textbook version, turning energies into probabilities needs a normalising constant over every possible input, which cannot easily be computed during training. It gets approximated by sampling instead, and how to make that cheap at scale is still being worked out.

Further reading Automatic Formal Verification for Code Generation (Logical Intelligence) · Proof assistant (Wikipedia) · Lean (proof assistant) (Wikipedia) · Energy-based model (Wikipedia)

Formal verification

Using mathematical proof, checked by a computer, to show a system does exactly what its specification says.

proof assistant

Software that helps a person build a formal proof and checks every step of it.

energy-based model

An AI model that scores how well a candidate answer fits, with low scores meaning a better fit.

undecidable

Impossible for any algorithm to answer correctly in every case.

token

A small chunk of text, often part of a word, that a language model reads and writes one at a time.

latent space

The internal numerical space where a model represents problems, rather than as words.

Lean

A proof assistant and programming language whose checker certifies that a proof is correct.

1. 1Formal verification · Wikipedia
2. 2Rice's theorem · Wikipedia
3. 3Frequently Asked Questions on seL4 · seL4 Foundation
4. 4seL4 explained, the 10,000-line kernel with a million lines of proof · Webiano
5. 5I-JEPA: The first AI model based on Yann LeCun's vision for more human-like AI · Meta AI
6. 6Energy-based model · Wikipedia
7. 7Energy-Based Models for Reasoning, LLMs for the Interface · Logical Intelligence
8. 8Automatic Formal Verification for Code Generation · Logical Intelligence
9. 9Logical Intelligence's Aleph Solves PutnamBench · Logical Intelligence
10. 10Proof assistant · Wikipedia
11. 11Lean (proof assistant) · Wikipedia