« Goedel-Prover » : différence entre les versions
(Page créée avec « ==en construction== == Définition == XXXXXXXXX == Français == ''' Goedel-Prover''' == Anglais == '''Goedel-Prover''' An open-source model for automated theorem proving. To overcome the scarcity of formal math data, they first trained models to convert 1.64 million natural language math problems into the formal language Lean 4. They then used an "expert iteration" process, where successive versions of the prover generate new proofs that are verified and... ») |
(Aucune différence)
|
Version du 4 août 2025 à 08:45
en construction
Définition
XXXXXXXXX
Français
Goedel-Prover
Anglais
Goedel-Prover
An open-source model for automated theorem proving. To overcome the scarcity of formal math data, they first trained models to convert 1.64 million natural language math problems into the formal language Lean 4. They then used an "expert iteration" process, where successive versions of the prover generate new proofs that are verified and added to the training set for the next iteration.
Source
Contributeurs: Arianne Arel, wiki
